open HolKernel bossLib word8Theory;

val _ = new_theory "tables";

val Sbox_def = Count.apply Define
 `(Sbox (F,F,F,F,F,F,F,F) = (F,T,T,F,F,F,T,T)) /\
  (Sbox (F,F,F,F,F,F,F,T) = (F,T,T,T,T,T,F,F)) /\
  (Sbox (F,F,F,F,F,F,T,F) = (F,T,T,T,F,T,T,T)) /\
  (Sbox (F,F,F,F,F,F,T,T) = (F,T,T,T,T,F,T,T)) /\
  (Sbox (F,F,F,F,F,T,F,F) = (T,T,T,T,F,F,T,F)) /\
  (Sbox (F,F,F,F,F,T,F,T) = (F,T,T,F,T,F,T,T)) /\
  (Sbox (F,F,F,F,F,T,T,F) = (F,T,T,F,T,T,T,T)) /\
  (Sbox (F,F,F,F,F,T,T,T) = (T,T,F,F,F,T,F,T)) /\
  (Sbox (F,F,F,F,T,F,F,F) = (F,F,T,T,F,F,F,F)) /\
  (Sbox (F,F,F,F,T,F,F,T) = (F,F,F,F,F,F,F,T)) /\
  (Sbox (F,F,F,F,T,F,T,F) = (F,T,T,F,F,T,T,T)) /\
  (Sbox (F,F,F,F,T,F,T,T) = (F,F,T,F,T,F,T,T)) /\
  (Sbox (F,F,F,F,T,T,F,F) = (T,T,T,T,T,T,T,F)) /\
  (Sbox (F,F,F,F,T,T,F,T) = (T,T,F,T,F,T,T,T)) /\
  (Sbox (F,F,F,F,T,T,T,F) = (T,F,T,F,T,F,T,T)) /\
  (Sbox (F,F,F,F,T,T,T,T) = (F,T,T,T,F,T,T,F)) /\
  (Sbox (F,F,F,T,F,F,F,F) = (T,T,F,F,T,F,T,F)) /\
  (Sbox (F,F,F,T,F,F,F,T) = (T,F,F,F,F,F,T,F)) /\
  (Sbox (F,F,F,T,F,F,T,F) = (T,T,F,F,T,F,F,T)) /\
  (Sbox (F,F,F,T,F,F,T,T) = (F,T,T,T,T,T,F,T)) /\
  (Sbox (F,F,F,T,F,T,F,F) = (T,T,T,T,T,F,T,F)) /\
  (Sbox (F,F,F,T,F,T,F,T) = (F,T,F,T,T,F,F,T)) /\
  (Sbox (F,F,F,T,F,T,T,F) = (F,T,F,F,F,T,T,T)) /\
  (Sbox (F,F,F,T,F,T,T,T) = (T,T,T,T,F,F,F,F)) /\
  (Sbox (F,F,F,T,T,F,F,F) = (T,F,T,F,T,T,F,T)) /\
  (Sbox (F,F,F,T,T,F,F,T) = (T,T,F,T,F,T,F,F)) /\
  (Sbox (F,F,F,T,T,F,T,F) = (T,F,T,F,F,F,T,F)) /\
  (Sbox (F,F,F,T,T,F,T,T) = (T,F,T,F,T,T,T,T)) /\
  (Sbox (F,F,F,T,T,T,F,F) = (T,F,F,T,T,T,F,F)) /\
  (Sbox (F,F,F,T,T,T,F,T) = (T,F,T,F,F,T,F,F)) /\
  (Sbox (F,F,F,T,T,T,T,F) = (F,T,T,T,F,F,T,F)) /\
  (Sbox (F,F,F,T,T,T,T,T) = (T,T,F,F,F,F,F,F)) /\
  (Sbox (F,F,T,F,F,F,F,F) = (T,F,T,T,F,T,T,T)) /\
  (Sbox (F,F,T,F,F,F,F,T) = (T,T,T,T,T,T,F,T)) /\
  (Sbox (F,F,T,F,F,F,T,F) = (T,F,F,T,F,F,T,T)) /\
  (Sbox (F,F,T,F,F,F,T,T) = (F,F,T,F,F,T,T,F)) /\
  (Sbox (F,F,T,F,F,T,F,F) = (F,F,T,T,F,T,T,F)) /\
  (Sbox (F,F,T,F,F,T,F,T) = (F,F,T,T,T,T,T,T)) /\
  (Sbox (F,F,T,F,F,T,T,F) = (T,T,T,T,F,T,T,T)) /\
  (Sbox (F,F,T,F,F,T,T,T) = (T,T,F,F,T,T,F,F)) /\
  (Sbox (F,F,T,F,T,F,F,F) = (F,F,T,T,F,T,F,F)) /\
  (Sbox (F,F,T,F,T,F,F,T) = (T,F,T,F,F,T,F,T)) /\
  (Sbox (F,F,T,F,T,F,T,F) = (T,T,T,F,F,T,F,T)) /\
  (Sbox (F,F,T,F,T,F,T,T) = (T,T,T,T,F,F,F,T)) /\
  (Sbox (F,F,T,F,T,T,F,F) = (F,T,T,T,F,F,F,T)) /\
  (Sbox (F,F,T,F,T,T,F,T) = (T,T,F,T,T,F,F,F)) /\
  (Sbox (F,F,T,F,T,T,T,F) = (F,F,T,T,F,F,F,T)) /\
  (Sbox (F,F,T,F,T,T,T,T) = (F,F,F,T,F,T,F,T)) /\
  (Sbox (F,F,T,T,F,F,F,F) = (F,F,F,F,F,T,F,F)) /\
  (Sbox (F,F,T,T,F,F,F,T) = (T,T,F,F,F,T,T,T)) /\
  (Sbox (F,F,T,T,F,F,T,F) = (F,F,T,F,F,F,T,T)) /\
  (Sbox (F,F,T,T,F,F,T,T) = (T,T,F,F,F,F,T,T)) /\
  (Sbox (F,F,T,T,F,T,F,F) = (F,F,F,T,T,F,F,F)) /\
  (Sbox (F,F,T,T,F,T,F,T) = (T,F,F,T,F,T,T,F)) /\
  (Sbox (F,F,T,T,F,T,T,F) = (F,F,F,F,F,T,F,T)) /\
  (Sbox (F,F,T,T,F,T,T,T) = (T,F,F,T,T,F,T,F)) /\
  (Sbox (F,F,T,T,T,F,F,F) = (F,F,F,F,F,T,T,T)) /\
  (Sbox (F,F,T,T,T,F,F,T) = (F,F,F,T,F,F,T,F)) /\
  (Sbox (F,F,T,T,T,F,T,F) = (T,F,F,F,F,F,F,F)) /\
  (Sbox (F,F,T,T,T,F,T,T) = (T,T,T,F,F,F,T,F)) /\
  (Sbox (F,F,T,T,T,T,F,F) = (T,T,T,F,T,F,T,T)) /\
  (Sbox (F,F,T,T,T,T,F,T) = (F,F,T,F,F,T,T,T)) /\
  (Sbox (F,F,T,T,T,T,T,F) = (T,F,T,T,F,F,T,F)) /\
  (Sbox (F,F,T,T,T,T,T,T) = (F,T,T,T,F,T,F,T)) /\
  (Sbox (F,T,F,F,F,F,F,F) = (F,F,F,F,T,F,F,T)) /\
  (Sbox (F,T,F,F,F,F,F,T) = (T,F,F,F,F,F,T,T)) /\
  (Sbox (F,T,F,F,F,F,T,F) = (F,F,T,F,T,T,F,F)) /\
  (Sbox (F,T,F,F,F,F,T,T) = (F,F,F,T,T,F,T,F)) /\
  (Sbox (F,T,F,F,F,T,F,F) = (F,F,F,T,T,F,T,T)) /\
  (Sbox (F,T,F,F,F,T,F,T) = (F,T,T,F,T,T,T,F)) /\
  (Sbox (F,T,F,F,F,T,T,F) = (F,T,F,T,T,F,T,F)) /\
  (Sbox (F,T,F,F,F,T,T,T) = (T,F,T,F,F,F,F,F)) /\
  (Sbox (F,T,F,F,T,F,F,F) = (F,T,F,T,F,F,T,F)) /\
  (Sbox (F,T,F,F,T,F,F,T) = (F,F,T,T,T,F,T,T)) /\
  (Sbox (F,T,F,F,T,F,T,F) = (T,T,F,T,F,T,T,F)) /\
  (Sbox (F,T,F,F,T,F,T,T) = (T,F,T,T,F,F,T,T)) /\
  (Sbox (F,T,F,F,T,T,F,F) = (F,F,T,F,T,F,F,T)) /\
  (Sbox (F,T,F,F,T,T,F,T) = (T,T,T,F,F,F,T,T)) /\
  (Sbox (F,T,F,F,T,T,T,F) = (F,F,T,F,T,T,T,T)) /\
  (Sbox (F,T,F,F,T,T,T,T) = (T,F,F,F,F,T,F,F)) /\
  (Sbox (F,T,F,T,F,F,F,F) = (F,T,F,T,F,F,T,T)) /\
  (Sbox (F,T,F,T,F,F,F,T) = (T,T,F,T,F,F,F,T)) /\
  (Sbox (F,T,F,T,F,F,T,F) = (F,F,F,F,F,F,F,F)) /\
  (Sbox (F,T,F,T,F,F,T,T) = (T,T,T,F,T,T,F,T)) /\
  (Sbox (F,T,F,T,F,T,F,F) = (F,F,T,F,F,F,F,F)) /\
  (Sbox (F,T,F,T,F,T,F,T) = (T,T,T,T,T,T,F,F)) /\
  (Sbox (F,T,F,T,F,T,T,F) = (T,F,T,T,F,F,F,T)) /\
  (Sbox (F,T,F,T,F,T,T,T) = (F,T,F,T,T,F,T,T)) /\
  (Sbox (F,T,F,T,T,F,F,F) = (F,T,T,F,T,F,T,F)) /\
  (Sbox (F,T,F,T,T,F,F,T) = (T,T,F,F,T,F,T,T)) /\
  (Sbox (F,T,F,T,T,F,T,F) = (T,F,T,T,T,T,T,F)) /\
  (Sbox (F,T,F,T,T,F,T,T) = (F,F,T,T,T,F,F,T)) /\
  (Sbox (F,T,F,T,T,T,F,F) = (F,T,F,F,T,F,T,F)) /\
  (Sbox (F,T,F,T,T,T,F,T) = (F,T,F,F,T,T,F,F)) /\
  (Sbox (F,T,F,T,T,T,T,F) = (F,T,F,T,T,F,F,F)) /\
  (Sbox (F,T,F,T,T,T,T,T) = (T,T,F,F,T,T,T,T)) /\
  (Sbox (F,T,T,F,F,F,F,F) = (T,T,F,T,F,F,F,F)) /\
  (Sbox (F,T,T,F,F,F,F,T) = (T,T,T,F,T,T,T,T)) /\
  (Sbox (F,T,T,F,F,F,T,F) = (T,F,T,F,T,F,T,F)) /\
  (Sbox (F,T,T,F,F,F,T,T) = (T,T,T,T,T,F,T,T)) /\
  (Sbox (F,T,T,F,F,T,F,F) = (F,T,F,F,F,F,T,T)) /\
  (Sbox (F,T,T,F,F,T,F,T) = (F,T,F,F,T,T,F,T)) /\
  (Sbox (F,T,T,F,F,T,T,F) = (F,F,T,T,F,F,T,T)) /\
  (Sbox (F,T,T,F,F,T,T,T) = (T,F,F,F,F,T,F,T)) /\
  (Sbox (F,T,T,F,T,F,F,F) = (F,T,F,F,F,T,F,T)) /\
  (Sbox (F,T,T,F,T,F,F,T) = (T,T,T,T,T,F,F,T)) /\
  (Sbox (F,T,T,F,T,F,T,F) = (F,F,F,F,F,F,T,F)) /\
  (Sbox (F,T,T,F,T,F,T,T) = (F,T,T,T,T,T,T,T)) /\
  (Sbox (F,T,T,F,T,T,F,F) = (F,T,F,T,F,F,F,F)) /\
  (Sbox (F,T,T,F,T,T,F,T) = (F,F,T,T,T,T,F,F)) /\
  (Sbox (F,T,T,F,T,T,T,F) = (T,F,F,T,T,T,T,T)) /\
  (Sbox (F,T,T,F,T,T,T,T) = (T,F,T,F,T,F,F,F)) /\
  (Sbox (F,T,T,T,F,F,F,F) = (F,T,F,T,F,F,F,T)) /\
  (Sbox (F,T,T,T,F,F,F,T) = (T,F,T,F,F,F,T,T)) /\
  (Sbox (F,T,T,T,F,F,T,F) = (F,T,F,F,F,F,F,F)) /\
  (Sbox (F,T,T,T,F,F,T,T) = (T,F,F,F,T,T,T,T)) /\
  (Sbox (F,T,T,T,F,T,F,F) = (T,F,F,T,F,F,T,F)) /\
  (Sbox (F,T,T,T,F,T,F,T) = (T,F,F,T,T,T,F,T)) /\
  (Sbox (F,T,T,T,F,T,T,F) = (F,F,T,T,T,F,F,F)) /\
  (Sbox (F,T,T,T,F,T,T,T) = (T,T,T,T,F,T,F,T)) /\
  (Sbox (F,T,T,T,T,F,F,F) = (T,F,T,T,T,T,F,F)) /\
  (Sbox (F,T,T,T,T,F,F,T) = (T,F,T,T,F,T,T,F)) /\
  (Sbox (F,T,T,T,T,F,T,F) = (T,T,F,T,T,F,T,F)) /\
  (Sbox (F,T,T,T,T,F,T,T) = (F,F,T,F,F,F,F,T)) /\
  (Sbox (F,T,T,T,T,T,F,F) = (F,F,F,T,F,F,F,F)) /\
  (Sbox (F,T,T,T,T,T,F,T) = (T,T,T,T,T,T,T,T)) /\
  (Sbox (F,T,T,T,T,T,T,F) = (T,T,T,T,F,F,T,T)) /\
  (Sbox (F,T,T,T,T,T,T,T) = (T,T,F,T,F,F,T,F)) /\
  (Sbox (T,F,F,F,F,F,F,F) = (T,T,F,F,T,T,F,T)) /\
  (Sbox (T,F,F,F,F,F,F,T) = (F,F,F,F,T,T,F,F)) /\
  (Sbox (T,F,F,F,F,F,T,F) = (F,F,F,T,F,F,T,T)) /\
  (Sbox (T,F,F,F,F,F,T,T) = (T,T,T,F,T,T,F,F)) /\
  (Sbox (T,F,F,F,F,T,F,F) = (F,T,F,T,T,T,T,T)) /\
  (Sbox (T,F,F,F,F,T,F,T) = (T,F,F,T,F,T,T,T)) /\
  (Sbox (T,F,F,F,F,T,T,F) = (F,T,F,F,F,T,F,F)) /\
  (Sbox (T,F,F,F,F,T,T,T) = (F,F,F,T,F,T,T,T)) /\
  (Sbox (T,F,F,F,T,F,F,F) = (T,T,F,F,F,T,F,F)) /\
  (Sbox (T,F,F,F,T,F,F,T) = (T,F,T,F,F,T,T,T)) /\
  (Sbox (T,F,F,F,T,F,T,F) = (F,T,T,T,T,T,T,F)) /\
  (Sbox (T,F,F,F,T,F,T,T) = (F,F,T,T,T,T,F,T)) /\
  (Sbox (T,F,F,F,T,T,F,F) = (F,T,T,F,F,T,F,F)) /\
  (Sbox (T,F,F,F,T,T,F,T) = (F,T,F,T,T,T,F,T)) /\
  (Sbox (T,F,F,F,T,T,T,F) = (F,F,F,T,T,F,F,T)) /\
  (Sbox (T,F,F,F,T,T,T,T) = (F,T,T,T,F,F,T,T)) /\
  (Sbox (T,F,F,T,F,F,F,F) = (F,T,T,F,F,F,F,F)) /\
  (Sbox (T,F,F,T,F,F,F,T) = (T,F,F,F,F,F,F,T)) /\
  (Sbox (T,F,F,T,F,F,T,F) = (F,T,F,F,T,T,T,T)) /\
  (Sbox (T,F,F,T,F,F,T,T) = (T,T,F,T,T,T,F,F)) /\
  (Sbox (T,F,F,T,F,T,F,F) = (F,F,T,F,F,F,T,F)) /\
  (Sbox (T,F,F,T,F,T,F,T) = (F,F,T,F,T,F,T,F)) /\
  (Sbox (T,F,F,T,F,T,T,F) = (T,F,F,T,F,F,F,F)) /\
  (Sbox (T,F,F,T,F,T,T,T) = (T,F,F,F,T,F,F,F)) /\
  (Sbox (T,F,F,T,T,F,F,F) = (F,T,F,F,F,T,T,F)) /\
  (Sbox (T,F,F,T,T,F,F,T) = (T,T,T,F,T,T,T,F)) /\
  (Sbox (T,F,F,T,T,F,T,F) = (T,F,T,T,T,F,F,F)) /\
  (Sbox (T,F,F,T,T,F,T,T) = (F,F,F,T,F,T,F,F)) /\
  (Sbox (T,F,F,T,T,T,F,F) = (T,T,F,T,T,T,T,F)) /\
  (Sbox (T,F,F,T,T,T,F,T) = (F,T,F,T,T,T,T,F)) /\
  (Sbox (T,F,F,T,T,T,T,F) = (F,F,F,F,T,F,T,T)) /\
  (Sbox (T,F,F,T,T,T,T,T) = (T,T,F,T,T,F,T,T)) /\
  (Sbox (T,F,T,F,F,F,F,F) = (T,T,T,F,F,F,F,F)) /\
  (Sbox (T,F,T,F,F,F,F,T) = (F,F,T,T,F,F,T,F)) /\
  (Sbox (T,F,T,F,F,F,T,F) = (F,F,T,T,T,F,T,F)) /\
  (Sbox (T,F,T,F,F,F,T,T) = (F,F,F,F,T,F,T,F)) /\
  (Sbox (T,F,T,F,F,T,F,F) = (F,T,F,F,T,F,F,T)) /\
  (Sbox (T,F,T,F,F,T,F,T) = (F,F,F,F,F,T,T,F)) /\
  (Sbox (T,F,T,F,F,T,T,F) = (F,F,T,F,F,T,F,F)) /\
  (Sbox (T,F,T,F,F,T,T,T) = (F,T,F,T,T,T,F,F)) /\
  (Sbox (T,F,T,F,T,F,F,F) = (T,T,F,F,F,F,T,F)) /\
  (Sbox (T,F,T,F,T,F,F,T) = (T,T,F,T,F,F,T,T)) /\
  (Sbox (T,F,T,F,T,F,T,F) = (T,F,T,F,T,T,F,F)) /\
  (Sbox (T,F,T,F,T,F,T,T) = (F,T,T,F,F,F,T,F)) /\
  (Sbox (T,F,T,F,T,T,F,F) = (T,F,F,T,F,F,F,T)) /\
  (Sbox (T,F,T,F,T,T,F,T) = (T,F,F,T,F,T,F,T)) /\
  (Sbox (T,F,T,F,T,T,T,F) = (T,T,T,F,F,T,F,F)) /\
  (Sbox (T,F,T,F,T,T,T,T) = (F,T,T,T,T,F,F,T)) /\
  (Sbox (T,F,T,T,F,F,F,F) = (T,T,T,F,F,T,T,T)) /\
  (Sbox (T,F,T,T,F,F,F,T) = (T,T,F,F,T,F,F,F)) /\
  (Sbox (T,F,T,T,F,F,T,F) = (F,F,T,T,F,T,T,T)) /\
  (Sbox (T,F,T,T,F,F,T,T) = (F,T,T,F,T,T,F,T)) /\
  (Sbox (T,F,T,T,F,T,F,F) = (T,F,F,F,T,T,F,T)) /\
  (Sbox (T,F,T,T,F,T,F,T) = (T,T,F,T,F,T,F,T)) /\
  (Sbox (T,F,T,T,F,T,T,F) = (F,T,F,F,T,T,T,F)) /\
  (Sbox (T,F,T,T,F,T,T,T) = (T,F,T,F,T,F,F,T)) /\
  (Sbox (T,F,T,T,T,F,F,F) = (F,T,T,F,T,T,F,F)) /\
  (Sbox (T,F,T,T,T,F,F,T) = (F,T,F,T,F,T,T,F)) /\
  (Sbox (T,F,T,T,T,F,T,F) = (T,T,T,T,F,T,F,F)) /\
  (Sbox (T,F,T,T,T,F,T,T) = (T,T,T,F,T,F,T,F)) /\
  (Sbox (T,F,T,T,T,T,F,F) = (F,T,T,F,F,T,F,T)) /\
  (Sbox (T,F,T,T,T,T,F,T) = (F,T,T,T,T,F,T,F)) /\
  (Sbox (T,F,T,T,T,T,T,F) = (T,F,T,F,T,T,T,F)) /\
  (Sbox (T,F,T,T,T,T,T,T) = (F,F,F,F,T,F,F,F)) /\
  (Sbox (T,T,F,F,F,F,F,F) = (T,F,T,T,T,F,T,F)) /\
  (Sbox (T,T,F,F,F,F,F,T) = (F,T,T,T,T,F,F,F)) /\
  (Sbox (T,T,F,F,F,F,T,F) = (F,F,T,F,F,T,F,T)) /\
  (Sbox (T,T,F,F,F,F,T,T) = (F,F,T,F,T,T,T,F)) /\
  (Sbox (T,T,F,F,F,T,F,F) = (F,F,F,T,T,T,F,F)) /\
  (Sbox (T,T,F,F,F,T,F,T) = (T,F,T,F,F,T,T,F)) /\
  (Sbox (T,T,F,F,F,T,T,F) = (T,F,T,T,F,T,F,F)) /\
  (Sbox (T,T,F,F,F,T,T,T) = (T,T,F,F,F,T,T,F)) /\
  (Sbox (T,T,F,F,T,F,F,F) = (T,T,T,F,T,F,F,F)) /\
  (Sbox (T,T,F,F,T,F,F,T) = (T,T,F,T,T,T,F,T)) /\
  (Sbox (T,T,F,F,T,F,T,F) = (F,T,T,T,F,T,F,F)) /\
  (Sbox (T,T,F,F,T,F,T,T) = (F,F,F,T,T,T,T,T)) /\
  (Sbox (T,T,F,F,T,T,F,F) = (F,T,F,F,T,F,T,T)) /\
  (Sbox (T,T,F,F,T,T,F,T) = (T,F,T,T,T,T,F,T)) /\
  (Sbox (T,T,F,F,T,T,T,F) = (T,F,F,F,T,F,T,T)) /\
  (Sbox (T,T,F,F,T,T,T,T) = (T,F,F,F,T,F,T,F)) /\
  (Sbox (T,T,F,T,F,F,F,F) = (F,T,T,T,F,F,F,F)) /\
  (Sbox (T,T,F,T,F,F,F,T) = (F,F,T,T,T,T,T,F)) /\
  (Sbox (T,T,F,T,F,F,T,F) = (T,F,T,T,F,T,F,T)) /\
  (Sbox (T,T,F,T,F,F,T,T) = (F,T,T,F,F,T,T,F)) /\
  (Sbox (T,T,F,T,F,T,F,F) = (F,T,F,F,T,F,F,F)) /\
  (Sbox (T,T,F,T,F,T,F,T) = (F,F,F,F,F,F,T,T)) /\
  (Sbox (T,T,F,T,F,T,T,F) = (T,T,T,T,F,T,T,F)) /\
  (Sbox (T,T,F,T,F,T,T,T) = (F,F,F,F,T,T,T,F)) /\
  (Sbox (T,T,F,T,T,F,F,F) = (F,T,T,F,F,F,F,T)) /\
  (Sbox (T,T,F,T,T,F,F,T) = (F,F,T,T,F,T,F,T)) /\
  (Sbox (T,T,F,T,T,F,T,F) = (F,T,F,T,F,T,T,T)) /\
  (Sbox (T,T,F,T,T,F,T,T) = (T,F,T,T,T,F,F,T)) /\
  (Sbox (T,T,F,T,T,T,F,F) = (T,F,F,F,F,T,T,F)) /\
  (Sbox (T,T,F,T,T,T,F,T) = (T,T,F,F,F,F,F,T)) /\
  (Sbox (T,T,F,T,T,T,T,F) = (F,F,F,T,T,T,F,T)) /\
  (Sbox (T,T,F,T,T,T,T,T) = (T,F,F,T,T,T,T,F)) /\
  (Sbox (T,T,T,F,F,F,F,F) = (T,T,T,F,F,F,F,T)) /\
  (Sbox (T,T,T,F,F,F,F,T) = (T,T,T,T,T,F,F,F)) /\
  (Sbox (T,T,T,F,F,F,T,F) = (T,F,F,T,T,F,F,F)) /\
  (Sbox (T,T,T,F,F,F,T,T) = (F,F,F,T,F,F,F,T)) /\
  (Sbox (T,T,T,F,F,T,F,F) = (F,T,T,F,T,F,F,T)) /\
  (Sbox (T,T,T,F,F,T,F,T) = (T,T,F,T,T,F,F,T)) /\
  (Sbox (T,T,T,F,F,T,T,F) = (T,F,F,F,T,T,T,F)) /\
  (Sbox (T,T,T,F,F,T,T,T) = (T,F,F,T,F,T,F,F)) /\
  (Sbox (T,T,T,F,T,F,F,F) = (T,F,F,T,T,F,T,T)) /\
  (Sbox (T,T,T,F,T,F,F,T) = (F,F,F,T,T,T,T,F)) /\
  (Sbox (T,T,T,F,T,F,T,F) = (T,F,F,F,F,T,T,T)) /\
  (Sbox (T,T,T,F,T,F,T,T) = (T,T,T,F,T,F,F,T)) /\
  (Sbox (T,T,T,F,T,T,F,F) = (T,T,F,F,T,T,T,F)) /\
  (Sbox (T,T,T,F,T,T,F,T) = (F,T,F,T,F,T,F,T)) /\
  (Sbox (T,T,T,F,T,T,T,F) = (F,F,T,F,T,F,F,F)) /\
  (Sbox (T,T,T,F,T,T,T,T) = (T,T,F,T,T,T,T,T)) /\
  (Sbox (T,T,T,T,F,F,F,F) = (T,F,F,F,T,T,F,F)) /\
  (Sbox (T,T,T,T,F,F,F,T) = (T,F,T,F,F,F,F,T)) /\
  (Sbox (T,T,T,T,F,F,T,F) = (T,F,F,F,T,F,F,T)) /\
  (Sbox (T,T,T,T,F,F,T,T) = (F,F,F,F,T,T,F,T)) /\
  (Sbox (T,T,T,T,F,T,F,F) = (T,F,T,T,T,T,T,T)) /\
  (Sbox (T,T,T,T,F,T,F,T) = (T,T,T,F,F,T,T,F)) /\
  (Sbox (T,T,T,T,F,T,T,F) = (F,T,F,F,F,F,T,F)) /\
  (Sbox (T,T,T,T,F,T,T,T) = (F,T,T,F,T,F,F,F)) /\
  (Sbox (T,T,T,T,T,F,F,F) = (F,T,F,F,F,F,F,T)) /\
  (Sbox (T,T,T,T,T,F,F,T) = (T,F,F,T,T,F,F,T)) /\
  (Sbox (T,T,T,T,T,F,T,F) = (F,F,T,F,T,T,F,T)) /\
  (Sbox (T,T,T,T,T,F,T,T) = (F,F,F,F,T,T,T,T)) /\
  (Sbox (T,T,T,T,T,T,F,F) = (T,F,T,T,F,F,F,F)) /\
  (Sbox (T,T,T,T,T,T,F,T) = (F,T,F,T,F,T,F,F)) /\
  (Sbox (T,T,T,T,T,T,T,F) = (T,F,T,T,T,F,T,T)) /\
  (Sbox (T,T,T,T,T,T,T,T) = (F,F,F,T,F,T,T,F))`;

val InvSbox_def = Count.apply Define
 `(InvSbox (F,F,F,F,F,F,F,F) = (F,T,F,T,F,F,T,F)) /\
  (InvSbox (F,F,F,F,F,F,F,T) = (F,F,F,F,T,F,F,T)) /\
  (InvSbox (F,F,F,F,F,F,T,F) = (F,T,T,F,T,F,T,F)) /\
  (InvSbox (F,F,F,F,F,F,T,T) = (T,T,F,T,F,T,F,T)) /\
  (InvSbox (F,F,F,F,F,T,F,F) = (F,F,T,T,F,F,F,F)) /\
  (InvSbox (F,F,F,F,F,T,F,T) = (F,F,T,T,F,T,T,F)) /\
  (InvSbox (F,F,F,F,F,T,T,F) = (T,F,T,F,F,T,F,T)) /\
  (InvSbox (F,F,F,F,F,T,T,T) = (F,F,T,T,T,F,F,F)) /\
  (InvSbox (F,F,F,F,T,F,F,F) = (T,F,T,T,T,T,T,T)) /\
  (InvSbox (F,F,F,F,T,F,F,T) = (F,T,F,F,F,F,F,F)) /\
  (InvSbox (F,F,F,F,T,F,T,F) = (T,F,T,F,F,F,T,T)) /\
  (InvSbox (F,F,F,F,T,F,T,T) = (T,F,F,T,T,T,T,F)) /\
  (InvSbox (F,F,F,F,T,T,F,F) = (T,F,F,F,F,F,F,T)) /\
  (InvSbox (F,F,F,F,T,T,F,T) = (T,T,T,T,F,F,T,T)) /\
  (InvSbox (F,F,F,F,T,T,T,F) = (T,T,F,T,F,T,T,T)) /\
  (InvSbox (F,F,F,F,T,T,T,T) = (T,T,T,T,T,F,T,T)) /\
  (InvSbox (F,F,F,T,F,F,F,F) = (F,T,T,T,T,T,F,F)) /\
  (InvSbox (F,F,F,T,F,F,F,T) = (T,T,T,F,F,F,T,T)) /\
  (InvSbox (F,F,F,T,F,F,T,F) = (F,F,T,T,T,F,F,T)) /\
  (InvSbox (F,F,F,T,F,F,T,T) = (T,F,F,F,F,F,T,F)) /\
  (InvSbox (F,F,F,T,F,T,F,F) = (T,F,F,T,T,F,T,T)) /\
  (InvSbox (F,F,F,T,F,T,F,T) = (F,F,T,F,T,T,T,T)) /\
  (InvSbox (F,F,F,T,F,T,T,F) = (T,T,T,T,T,T,T,T)) /\
  (InvSbox (F,F,F,T,F,T,T,T) = (T,F,F,F,F,T,T,T)) /\
  (InvSbox (F,F,F,T,T,F,F,F) = (F,F,T,T,F,T,F,F)) /\
  (InvSbox (F,F,F,T,T,F,F,T) = (T,F,F,F,T,T,T,F)) /\
  (InvSbox (F,F,F,T,T,F,T,F) = (F,T,F,F,F,F,T,T)) /\
  (InvSbox (F,F,F,T,T,F,T,T) = (F,T,F,F,F,T,F,F)) /\
  (InvSbox (F,F,F,T,T,T,F,F) = (T,T,F,F,F,T,F,F)) /\
  (InvSbox (F,F,F,T,T,T,F,T) = (T,T,F,T,T,T,T,F)) /\
  (InvSbox (F,F,F,T,T,T,T,F) = (T,T,T,F,T,F,F,T)) /\
  (InvSbox (F,F,F,T,T,T,T,T) = (T,T,F,F,T,F,T,T)) /\
  (InvSbox (F,F,T,F,F,F,F,F) = (F,T,F,T,F,T,F,F)) /\
  (InvSbox (F,F,T,F,F,F,F,T) = (F,T,T,T,T,F,T,T)) /\
  (InvSbox (F,F,T,F,F,F,T,F) = (T,F,F,T,F,T,F,F)) /\
  (InvSbox (F,F,T,F,F,F,T,T) = (F,F,T,T,F,F,T,F)) /\
  (InvSbox (F,F,T,F,F,T,F,F) = (T,F,T,F,F,T,T,F)) /\
  (InvSbox (F,F,T,F,F,T,F,T) = (T,T,F,F,F,F,T,F)) /\
  (InvSbox (F,F,T,F,F,T,T,F) = (F,F,T,F,F,F,T,T)) /\
  (InvSbox (F,F,T,F,F,T,T,T) = (F,F,T,T,T,T,F,T)) /\
  (InvSbox (F,F,T,F,T,F,F,F) = (T,T,T,F,T,T,T,F)) /\
  (InvSbox (F,F,T,F,T,F,F,T) = (F,T,F,F,T,T,F,F)) /\
  (InvSbox (F,F,T,F,T,F,T,F) = (T,F,F,T,F,T,F,T)) /\
  (InvSbox (F,F,T,F,T,F,T,T) = (F,F,F,F,T,F,T,T)) /\
  (InvSbox (F,F,T,F,T,T,F,F) = (F,T,F,F,F,F,T,F)) /\
  (InvSbox (F,F,T,F,T,T,F,T) = (T,T,T,T,T,F,T,F)) /\
  (InvSbox (F,F,T,F,T,T,T,F) = (T,T,F,F,F,F,T,T)) /\
  (InvSbox (F,F,T,F,T,T,T,T) = (F,T,F,F,T,T,T,F)) /\
  (InvSbox (F,F,T,T,F,F,F,F) = (F,F,F,F,T,F,F,F)) /\
  (InvSbox (F,F,T,T,F,F,F,T) = (F,F,T,F,T,T,T,F)) /\
  (InvSbox (F,F,T,T,F,F,T,F) = (T,F,T,F,F,F,F,T)) /\
  (InvSbox (F,F,T,T,F,F,T,T) = (F,T,T,F,F,T,T,F)) /\
  (InvSbox (F,F,T,T,F,T,F,F) = (F,F,T,F,T,F,F,F)) /\
  (InvSbox (F,F,T,T,F,T,F,T) = (T,T,F,T,T,F,F,T)) /\
  (InvSbox (F,F,T,T,F,T,T,F) = (F,F,T,F,F,T,F,F)) /\
  (InvSbox (F,F,T,T,F,T,T,T) = (T,F,T,T,F,F,T,F)) /\
  (InvSbox (F,F,T,T,T,F,F,F) = (F,T,T,T,F,T,T,F)) /\
  (InvSbox (F,F,T,T,T,F,F,T) = (F,T,F,T,T,F,T,T)) /\
  (InvSbox (F,F,T,T,T,F,T,F) = (T,F,T,F,F,F,T,F)) /\
  (InvSbox (F,F,T,T,T,F,T,T) = (F,T,F,F,T,F,F,T)) /\
  (InvSbox (F,F,T,T,T,T,F,F) = (F,T,T,F,T,T,F,T)) /\
  (InvSbox (F,F,T,T,T,T,F,T) = (T,F,F,F,T,F,T,T)) /\
  (InvSbox (F,F,T,T,T,T,T,F) = (T,T,F,T,F,F,F,T)) /\
  (InvSbox (F,F,T,T,T,T,T,T) = (F,F,T,F,F,T,F,T)) /\
  (InvSbox (F,T,F,F,F,F,F,F) = (F,T,T,T,F,F,T,F)) /\
  (InvSbox (F,T,F,F,F,F,F,T) = (T,T,T,T,T,F,F,F)) /\
  (InvSbox (F,T,F,F,F,F,T,F) = (T,T,T,T,F,T,T,F)) /\
  (InvSbox (F,T,F,F,F,F,T,T) = (F,T,T,F,F,T,F,F)) /\
  (InvSbox (F,T,F,F,F,T,F,F) = (T,F,F,F,F,T,T,F)) /\
  (InvSbox (F,T,F,F,F,T,F,T) = (F,T,T,F,T,F,F,F)) /\
  (InvSbox (F,T,F,F,F,T,T,F) = (T,F,F,T,T,F,F,F)) /\
  (InvSbox (F,T,F,F,F,T,T,T) = (F,F,F,T,F,T,T,F)) /\
  (InvSbox (F,T,F,F,T,F,F,F) = (T,T,F,T,F,T,F,F)) /\
  (InvSbox (F,T,F,F,T,F,F,T) = (T,F,T,F,F,T,F,F)) /\
  (InvSbox (F,T,F,F,T,F,T,F) = (F,T,F,T,T,T,F,F)) /\
  (InvSbox (F,T,F,F,T,F,T,T) = (T,T,F,F,T,T,F,F)) /\
  (InvSbox (F,T,F,F,T,T,F,F) = (F,T,F,T,T,T,F,T)) /\
  (InvSbox (F,T,F,F,T,T,F,T) = (F,T,T,F,F,T,F,T)) /\
  (InvSbox (F,T,F,F,T,T,T,F) = (T,F,T,T,F,T,T,F)) /\
  (InvSbox (F,T,F,F,T,T,T,T) = (T,F,F,T,F,F,T,F)) /\
  (InvSbox (F,T,F,T,F,F,F,F) = (F,T,T,F,T,T,F,F)) /\
  (InvSbox (F,T,F,T,F,F,F,T) = (F,T,T,T,F,F,F,F)) /\
  (InvSbox (F,T,F,T,F,F,T,F) = (F,T,F,F,T,F,F,F)) /\
  (InvSbox (F,T,F,T,F,F,T,T) = (F,T,F,T,F,F,F,F)) /\
  (InvSbox (F,T,F,T,F,T,F,F) = (T,T,T,T,T,T,F,T)) /\
  (InvSbox (F,T,F,T,F,T,F,T) = (T,T,T,F,T,T,F,T)) /\
  (InvSbox (F,T,F,T,F,T,T,F) = (T,F,T,T,T,F,F,T)) /\
  (InvSbox (F,T,F,T,F,T,T,T) = (T,T,F,T,T,F,T,F)) /\
  (InvSbox (F,T,F,T,T,F,F,F) = (F,T,F,T,T,T,T,F)) /\
  (InvSbox (F,T,F,T,T,F,F,T) = (F,F,F,T,F,T,F,T)) /\
  (InvSbox (F,T,F,T,T,F,T,F) = (F,T,F,F,F,T,T,F)) /\
  (InvSbox (F,T,F,T,T,F,T,T) = (F,T,F,T,F,T,T,T)) /\
  (InvSbox (F,T,F,T,T,T,F,F) = (T,F,T,F,F,T,T,T)) /\
  (InvSbox (F,T,F,T,T,T,F,T) = (T,F,F,F,T,T,F,T)) /\
  (InvSbox (F,T,F,T,T,T,T,F) = (T,F,F,T,T,T,F,T)) /\
  (InvSbox (F,T,F,T,T,T,T,T) = (T,F,F,F,F,T,F,F)) /\
  (InvSbox (F,T,T,F,F,F,F,F) = (T,F,F,T,F,F,F,F)) /\
  (InvSbox (F,T,T,F,F,F,F,T) = (T,T,F,T,T,F,F,F)) /\
  (InvSbox (F,T,T,F,F,F,T,F) = (T,F,T,F,T,F,T,T)) /\
  (InvSbox (F,T,T,F,F,F,T,T) = (F,F,F,F,F,F,F,F)) /\
  (InvSbox (F,T,T,F,F,T,F,F) = (T,F,F,F,T,T,F,F)) /\
  (InvSbox (F,T,T,F,F,T,F,T) = (T,F,T,T,T,T,F,F)) /\
  (InvSbox (F,T,T,F,F,T,T,F) = (T,T,F,T,F,F,T,T)) /\
  (InvSbox (F,T,T,F,F,T,T,T) = (F,F,F,F,T,F,T,F)) /\
  (InvSbox (F,T,T,F,T,F,F,F) = (T,T,T,T,F,T,T,T)) /\
  (InvSbox (F,T,T,F,T,F,F,T) = (T,T,T,F,F,T,F,F)) /\
  (InvSbox (F,T,T,F,T,F,T,F) = (F,T,F,T,T,F,F,F)) /\
  (InvSbox (F,T,T,F,T,F,T,T) = (F,F,F,F,F,T,F,T)) /\
  (InvSbox (F,T,T,F,T,T,F,F) = (T,F,T,T,T,F,F,F)) /\
  (InvSbox (F,T,T,F,T,T,F,T) = (T,F,T,T,F,F,T,T)) /\
  (InvSbox (F,T,T,F,T,T,T,F) = (F,T,F,F,F,T,F,T)) /\
  (InvSbox (F,T,T,F,T,T,T,T) = (F,F,F,F,F,T,T,F)) /\
  (InvSbox (F,T,T,T,F,F,F,F) = (T,T,F,T,F,F,F,F)) /\
  (InvSbox (F,T,T,T,F,F,F,T) = (F,F,T,F,T,T,F,F)) /\
  (InvSbox (F,T,T,T,F,F,T,F) = (F,F,F,T,T,T,T,F)) /\
  (InvSbox (F,T,T,T,F,F,T,T) = (T,F,F,F,T,T,T,T)) /\
  (InvSbox (F,T,T,T,F,T,F,F) = (T,T,F,F,T,F,T,F)) /\
  (InvSbox (F,T,T,T,F,T,F,T) = (F,F,T,T,T,T,T,T)) /\
  (InvSbox (F,T,T,T,F,T,T,F) = (F,F,F,F,T,T,T,T)) /\
  (InvSbox (F,T,T,T,F,T,T,T) = (F,F,F,F,F,F,T,F)) /\
  (InvSbox (F,T,T,T,T,F,F,F) = (T,T,F,F,F,F,F,T)) /\
  (InvSbox (F,T,T,T,T,F,F,T) = (T,F,T,F,T,T,T,T)) /\
  (InvSbox (F,T,T,T,T,F,T,F) = (T,F,T,T,T,T,F,T)) /\
  (InvSbox (F,T,T,T,T,F,T,T) = (F,F,F,F,F,F,T,T)) /\
  (InvSbox (F,T,T,T,T,T,F,F) = (F,F,F,F,F,F,F,T)) /\
  (InvSbox (F,T,T,T,T,T,F,T) = (F,F,F,T,F,F,T,T)) /\
  (InvSbox (F,T,T,T,T,T,T,F) = (T,F,F,F,T,F,T,F)) /\
  (InvSbox (F,T,T,T,T,T,T,T) = (F,T,T,F,T,F,T,T)) /\
  (InvSbox (T,F,F,F,F,F,F,F) = (F,F,T,T,T,F,T,F)) /\
  (InvSbox (T,F,F,F,F,F,F,T) = (T,F,F,T,F,F,F,T)) /\
  (InvSbox (T,F,F,F,F,F,T,F) = (F,F,F,T,F,F,F,T)) /\
  (InvSbox (T,F,F,F,F,F,T,T) = (F,T,F,F,F,F,F,T)) /\
  (InvSbox (T,F,F,F,F,T,F,F) = (F,T,F,F,T,T,T,T)) /\
  (InvSbox (T,F,F,F,F,T,F,T) = (F,T,T,F,F,T,T,T)) /\
  (InvSbox (T,F,F,F,F,T,T,F) = (T,T,F,T,T,T,F,F)) /\
  (InvSbox (T,F,F,F,F,T,T,T) = (T,T,T,F,T,F,T,F)) /\
  (InvSbox (T,F,F,F,T,F,F,F) = (T,F,F,T,F,T,T,T)) /\
  (InvSbox (T,F,F,F,T,F,F,T) = (T,T,T,T,F,F,T,F)) /\
  (InvSbox (T,F,F,F,T,F,T,F) = (T,T,F,F,T,T,T,T)) /\
  (InvSbox (T,F,F,F,T,F,T,T) = (T,T,F,F,T,T,T,F)) /\
  (InvSbox (T,F,F,F,T,T,F,F) = (T,T,T,T,F,F,F,F)) /\
  (InvSbox (T,F,F,F,T,T,F,T) = (T,F,T,T,F,T,F,F)) /\
  (InvSbox (T,F,F,F,T,T,T,F) = (T,T,T,F,F,T,T,F)) /\
  (InvSbox (T,F,F,F,T,T,T,T) = (F,T,T,T,F,F,T,T)) /\
  (InvSbox (T,F,F,T,F,F,F,F) = (T,F,F,T,F,T,T,F)) /\
  (InvSbox (T,F,F,T,F,F,F,T) = (T,F,T,F,T,T,F,F)) /\
  (InvSbox (T,F,F,T,F,F,T,F) = (F,T,T,T,F,T,F,F)) /\
  (InvSbox (T,F,F,T,F,F,T,T) = (F,F,T,F,F,F,T,F)) /\
  (InvSbox (T,F,F,T,F,T,F,F) = (T,T,T,F,F,T,T,T)) /\
  (InvSbox (T,F,F,T,F,T,F,T) = (T,F,T,F,T,T,F,T)) /\
  (InvSbox (T,F,F,T,F,T,T,F) = (F,F,T,T,F,T,F,T)) /\
  (InvSbox (T,F,F,T,F,T,T,T) = (T,F,F,F,F,T,F,T)) /\
  (InvSbox (T,F,F,T,T,F,F,F) = (T,T,T,F,F,F,T,F)) /\
  (InvSbox (T,F,F,T,T,F,F,T) = (T,T,T,T,T,F,F,T)) /\
  (InvSbox (T,F,F,T,T,F,T,F) = (F,F,T,T,F,T,T,T)) /\
  (InvSbox (T,F,F,T,T,F,T,T) = (T,T,T,F,T,F,F,F)) /\
  (InvSbox (T,F,F,T,T,T,F,F) = (F,F,F,T,T,T,F,F)) /\
  (InvSbox (T,F,F,T,T,T,F,T) = (F,T,T,T,F,T,F,T)) /\
  (InvSbox (T,F,F,T,T,T,T,F) = (T,T,F,T,T,T,T,T)) /\
  (InvSbox (T,F,F,T,T,T,T,T) = (F,T,T,F,T,T,T,F)) /\
  (InvSbox (T,F,T,F,F,F,F,F) = (F,T,F,F,F,T,T,T)) /\
  (InvSbox (T,F,T,F,F,F,F,T) = (T,T,T,T,F,F,F,T)) /\
  (InvSbox (T,F,T,F,F,F,T,F) = (F,F,F,T,T,F,T,F)) /\
  (InvSbox (T,F,T,F,F,F,T,T) = (F,T,T,T,F,F,F,T)) /\
  (InvSbox (T,F,T,F,F,T,F,F) = (F,F,F,T,T,T,F,T)) /\
  (InvSbox (T,F,T,F,F,T,F,T) = (F,F,T,F,T,F,F,T)) /\
  (InvSbox (T,F,T,F,F,T,T,F) = (T,T,F,F,F,T,F,T)) /\
  (InvSbox (T,F,T,F,F,T,T,T) = (T,F,F,F,T,F,F,T)) /\
  (InvSbox (T,F,T,F,T,F,F,F) = (F,T,T,F,T,T,T,T)) /\
  (InvSbox (T,F,T,F,T,F,F,T) = (T,F,T,T,F,T,T,T)) /\
  (InvSbox (T,F,T,F,T,F,T,F) = (F,T,T,F,F,F,T,F)) /\
  (InvSbox (T,F,T,F,T,F,T,T) = (F,F,F,F,T,T,T,F)) /\
  (InvSbox (T,F,T,F,T,T,F,F) = (T,F,T,F,T,F,T,F)) /\
  (InvSbox (T,F,T,F,T,T,F,T) = (F,F,F,T,T,F,F,F)) /\
  (InvSbox (T,F,T,F,T,T,T,F) = (T,F,T,T,T,T,T,F)) /\
  (InvSbox (T,F,T,F,T,T,T,T) = (F,F,F,T,T,F,T,T)) /\
  (InvSbox (T,F,T,T,F,F,F,F) = (T,T,T,T,T,T,F,F)) /\
  (InvSbox (T,F,T,T,F,F,F,T) = (F,T,F,T,F,T,T,F)) /\
  (InvSbox (T,F,T,T,F,F,T,F) = (F,F,T,T,T,T,T,F)) /\
  (InvSbox (T,F,T,T,F,F,T,T) = (F,T,F,F,T,F,T,T)) /\
  (InvSbox (T,F,T,T,F,T,F,F) = (T,T,F,F,F,T,T,F)) /\
  (InvSbox (T,F,T,T,F,T,F,T) = (T,T,F,T,F,F,T,F)) /\
  (InvSbox (T,F,T,T,F,T,T,F) = (F,T,T,T,T,F,F,T)) /\
  (InvSbox (T,F,T,T,F,T,T,T) = (F,F,T,F,F,F,F,F)) /\
  (InvSbox (T,F,T,T,T,F,F,F) = (T,F,F,T,T,F,T,F)) /\
  (InvSbox (T,F,T,T,T,F,F,T) = (T,T,F,T,T,F,T,T)) /\
  (InvSbox (T,F,T,T,T,F,T,F) = (T,T,F,F,F,F,F,F)) /\
  (InvSbox (T,F,T,T,T,F,T,T) = (T,T,T,T,T,T,T,F)) /\
  (InvSbox (T,F,T,T,T,T,F,F) = (F,T,T,T,T,F,F,F)) /\
  (InvSbox (T,F,T,T,T,T,F,T) = (T,T,F,F,T,T,F,T)) /\
  (InvSbox (T,F,T,T,T,T,T,F) = (F,T,F,T,T,F,T,F)) /\
  (InvSbox (T,F,T,T,T,T,T,T) = (T,T,T,T,F,T,F,F)) /\
  (InvSbox (T,T,F,F,F,F,F,F) = (F,F,F,T,T,T,T,T)) /\
  (InvSbox (T,T,F,F,F,F,F,T) = (T,T,F,T,T,T,F,T)) /\
  (InvSbox (T,T,F,F,F,F,T,F) = (T,F,T,F,T,F,F,F)) /\
  (InvSbox (T,T,F,F,F,F,T,T) = (F,F,T,T,F,F,T,T)) /\
  (InvSbox (T,T,F,F,F,T,F,F) = (T,F,F,F,T,F,F,F)) /\
  (InvSbox (T,T,F,F,F,T,F,T) = (F,F,F,F,F,T,T,T)) /\
  (InvSbox (T,T,F,F,F,T,T,F) = (T,T,F,F,F,T,T,T)) /\
  (InvSbox (T,T,F,F,F,T,T,T) = (F,F,T,T,F,F,F,T)) /\
  (InvSbox (T,T,F,F,T,F,F,F) = (T,F,T,T,F,F,F,T)) /\
  (InvSbox (T,T,F,F,T,F,F,T) = (F,F,F,T,F,F,T,F)) /\
  (InvSbox (T,T,F,F,T,F,T,F) = (F,F,F,T,F,F,F,F)) /\
  (InvSbox (T,T,F,F,T,F,T,T) = (F,T,F,T,T,F,F,T)) /\
  (InvSbox (T,T,F,F,T,T,F,F) = (F,F,T,F,F,T,T,T)) /\
  (InvSbox (T,T,F,F,T,T,F,T) = (T,F,F,F,F,F,F,F)) /\
  (InvSbox (T,T,F,F,T,T,T,F) = (T,T,T,F,T,T,F,F)) /\
  (InvSbox (T,T,F,F,T,T,T,T) = (F,T,F,T,T,T,T,T)) /\
  (InvSbox (T,T,F,T,F,F,F,F) = (F,T,T,F,F,F,F,F)) /\
  (InvSbox (T,T,F,T,F,F,F,T) = (F,T,F,T,F,F,F,T)) /\
  (InvSbox (T,T,F,T,F,F,T,F) = (F,T,T,T,T,T,T,T)) /\
  (InvSbox (T,T,F,T,F,F,T,T) = (T,F,T,F,T,F,F,T)) /\
  (InvSbox (T,T,F,T,F,T,F,F) = (F,F,F,T,T,F,F,T)) /\
  (InvSbox (T,T,F,T,F,T,F,T) = (T,F,T,T,F,T,F,T)) /\
  (InvSbox (T,T,F,T,F,T,T,F) = (F,T,F,F,T,F,T,F)) /\
  (InvSbox (T,T,F,T,F,T,T,T) = (F,F,F,F,T,T,F,T)) /\
  (InvSbox (T,T,F,T,T,F,F,F) = (F,F,T,F,T,T,F,T)) /\
  (InvSbox (T,T,F,T,T,F,F,T) = (T,T,T,F,F,T,F,T)) /\
  (InvSbox (T,T,F,T,T,F,T,F) = (F,T,T,T,T,F,T,F)) /\
  (InvSbox (T,T,F,T,T,F,T,T) = (T,F,F,T,T,T,T,T)) /\
  (InvSbox (T,T,F,T,T,T,F,F) = (T,F,F,T,F,F,T,T)) /\
  (InvSbox (T,T,F,T,T,T,F,T) = (T,T,F,F,T,F,F,T)) /\
  (InvSbox (T,T,F,T,T,T,T,F) = (T,F,F,T,T,T,F,F)) /\
  (InvSbox (T,T,F,T,T,T,T,T) = (T,T,T,F,T,T,T,T)) /\
  (InvSbox (T,T,T,F,F,F,F,F) = (T,F,T,F,F,F,F,F)) /\
  (InvSbox (T,T,T,F,F,F,F,T) = (T,T,T,F,F,F,F,F)) /\
  (InvSbox (T,T,T,F,F,F,T,F) = (F,F,T,T,T,F,T,T)) /\
  (InvSbox (T,T,T,F,F,F,T,T) = (F,T,F,F,T,T,F,T)) /\
  (InvSbox (T,T,T,F,F,T,F,F) = (T,F,T,F,T,T,T,F)) /\
  (InvSbox (T,T,T,F,F,T,F,T) = (F,F,T,F,T,F,T,F)) /\
  (InvSbox (T,T,T,F,F,T,T,F) = (T,T,T,T,F,T,F,T)) /\
  (InvSbox (T,T,T,F,F,T,T,T) = (T,F,T,T,F,F,F,F)) /\
  (InvSbox (T,T,T,F,T,F,F,F) = (T,T,F,F,T,F,F,F)) /\
  (InvSbox (T,T,T,F,T,F,F,T) = (T,T,T,F,T,F,T,T)) /\
  (InvSbox (T,T,T,F,T,F,T,F) = (T,F,T,T,T,F,T,T)) /\
  (InvSbox (T,T,T,F,T,F,T,T) = (F,F,T,T,T,T,F,F)) /\
  (InvSbox (T,T,T,F,T,T,F,F) = (T,F,F,F,F,F,T,T)) /\
  (InvSbox (T,T,T,F,T,T,F,T) = (F,T,F,T,F,F,T,T)) /\
  (InvSbox (T,T,T,F,T,T,T,F) = (T,F,F,T,T,F,F,T)) /\
  (InvSbox (T,T,T,F,T,T,T,T) = (F,T,T,F,F,F,F,T)) /\
  (InvSbox (T,T,T,T,F,F,F,F) = (F,F,F,T,F,T,T,T)) /\
  (InvSbox (T,T,T,T,F,F,F,T) = (F,F,T,F,T,F,T,T)) /\
  (InvSbox (T,T,T,T,F,F,T,F) = (F,F,F,F,F,T,F,F)) /\
  (InvSbox (T,T,T,T,F,F,T,T) = (F,T,T,T,T,T,T,F)) /\
  (InvSbox (T,T,T,T,F,T,F,F) = (T,F,T,T,T,F,T,F)) /\
  (InvSbox (T,T,T,T,F,T,F,T) = (F,T,T,T,F,T,T,T)) /\
  (InvSbox (T,T,T,T,F,T,T,F) = (T,T,F,T,F,T,T,F)) /\
  (InvSbox (T,T,T,T,F,T,T,T) = (F,F,T,F,F,T,T,F)) /\
  (InvSbox (T,T,T,T,T,F,F,F) = (T,T,T,F,F,F,F,T)) /\
  (InvSbox (T,T,T,T,T,F,F,T) = (F,T,T,F,T,F,F,T)) /\
  (InvSbox (T,T,T,T,T,F,T,F) = (F,F,F,T,F,T,F,F)) /\
  (InvSbox (T,T,T,T,T,F,T,T) = (F,T,T,F,F,F,T,T)) /\
  (InvSbox (T,T,T,T,T,T,F,F) = (F,T,F,T,F,T,F,T)) /\
  (InvSbox (T,T,T,T,T,T,F,T) = (F,F,T,F,F,F,F,T)) /\
  (InvSbox (T,T,T,T,T,T,T,F) = (F,F,F,F,T,T,F,F)) /\
  (InvSbox (T,T,T,T,T,T,T,T) = (F,T,T,T,T,T,F,T))`;

val GF256_by_2_def = Count.apply Define
 `(GF256_by_2 (F,F,F,F,F,F,F,F) = (F,F,F,F,F,F,F,F)) /\
  (GF256_by_2 (F,F,F,F,F,F,F,T) = (F,F,F,F,F,F,T,F)) /\
  (GF256_by_2 (F,F,F,F,F,F,T,F) = (F,F,F,F,F,T,F,F)) /\
  (GF256_by_2 (F,F,F,F,F,F,T,T) = (F,F,F,F,F,T,T,F)) /\
  (GF256_by_2 (F,F,F,F,F,T,F,F) = (F,F,F,F,T,F,F,F)) /\
  (GF256_by_2 (F,F,F,F,F,T,F,T) = (F,F,F,F,T,F,T,F)) /\
  (GF256_by_2 (F,F,F,F,F,T,T,F) = (F,F,F,F,T,T,F,F)) /\
  (GF256_by_2 (F,F,F,F,F,T,T,T) = (F,F,F,F,T,T,T,F)) /\
  (GF256_by_2 (F,F,F,F,T,F,F,F) = (F,F,F,T,F,F,F,F)) /\
  (GF256_by_2 (F,F,F,F,T,F,F,T) = (F,F,F,T,F,F,T,F)) /\
  (GF256_by_2 (F,F,F,F,T,F,T,F) = (F,F,F,T,F,T,F,F)) /\
  (GF256_by_2 (F,F,F,F,T,F,T,T) = (F,F,F,T,F,T,T,F)) /\
  (GF256_by_2 (F,F,F,F,T,T,F,F) = (F,F,F,T,T,F,F,F)) /\
  (GF256_by_2 (F,F,F,F,T,T,F,T) = (F,F,F,T,T,F,T,F)) /\
  (GF256_by_2 (F,F,F,F,T,T,T,F) = (F,F,F,T,T,T,F,F)) /\
  (GF256_by_2 (F,F,F,F,T,T,T,T) = (F,F,F,T,T,T,T,F)) /\
  (GF256_by_2 (F,F,F,T,F,F,F,F) = (F,F,T,F,F,F,F,F)) /\
  (GF256_by_2 (F,F,F,T,F,F,F,T) = (F,F,T,F,F,F,T,F)) /\
  (GF256_by_2 (F,F,F,T,F,F,T,F) = (F,F,T,F,F,T,F,F)) /\
  (GF256_by_2 (F,F,F,T,F,F,T,T) = (F,F,T,F,F,T,T,F)) /\
  (GF256_by_2 (F,F,F,T,F,T,F,F) = (F,F,T,F,T,F,F,F)) /\
  (GF256_by_2 (F,F,F,T,F,T,F,T) = (F,F,T,F,T,F,T,F)) /\
  (GF256_by_2 (F,F,F,T,F,T,T,F) = (F,F,T,F,T,T,F,F)) /\
  (GF256_by_2 (F,F,F,T,F,T,T,T) = (F,F,T,F,T,T,T,F)) /\
  (GF256_by_2 (F,F,F,T,T,F,F,F) = (F,F,T,T,F,F,F,F)) /\
  (GF256_by_2 (F,F,F,T,T,F,F,T) = (F,F,T,T,F,F,T,F)) /\
  (GF256_by_2 (F,F,F,T,T,F,T,F) = (F,F,T,T,F,T,F,F)) /\
  (GF256_by_2 (F,F,F,T,T,F,T,T) = (F,F,T,T,F,T,T,F)) /\
  (GF256_by_2 (F,F,F,T,T,T,F,F) = (F,F,T,T,T,F,F,F)) /\
  (GF256_by_2 (F,F,F,T,T,T,F,T) = (F,F,T,T,T,F,T,F)) /\
  (GF256_by_2 (F,F,F,T,T,T,T,F) = (F,F,T,T,T,T,F,F)) /\
  (GF256_by_2 (F,F,F,T,T,T,T,T) = (F,F,T,T,T,T,T,F)) /\
  (GF256_by_2 (F,F,T,F,F,F,F,F) = (F,T,F,F,F,F,F,F)) /\
  (GF256_by_2 (F,F,T,F,F,F,F,T) = (F,T,F,F,F,F,T,F)) /\
  (GF256_by_2 (F,F,T,F,F,F,T,F) = (F,T,F,F,F,T,F,F)) /\
  (GF256_by_2 (F,F,T,F,F,F,T,T) = (F,T,F,F,F,T,T,F)) /\
  (GF256_by_2 (F,F,T,F,F,T,F,F) = (F,T,F,F,T,F,F,F)) /\
  (GF256_by_2 (F,F,T,F,F,T,F,T) = (F,T,F,F,T,F,T,F)) /\
  (GF256_by_2 (F,F,T,F,F,T,T,F) = (F,T,F,F,T,T,F,F)) /\
  (GF256_by_2 (F,F,T,F,F,T,T,T) = (F,T,F,F,T,T,T,F)) /\
  (GF256_by_2 (F,F,T,F,T,F,F,F) = (F,T,F,T,F,F,F,F)) /\
  (GF256_by_2 (F,F,T,F,T,F,F,T) = (F,T,F,T,F,F,T,F)) /\
  (GF256_by_2 (F,F,T,F,T,F,T,F) = (F,T,F,T,F,T,F,F)) /\
  (GF256_by_2 (F,F,T,F,T,F,T,T) = (F,T,F,T,F,T,T,F)) /\
  (GF256_by_2 (F,F,T,F,T,T,F,F) = (F,T,F,T,T,F,F,F)) /\
  (GF256_by_2 (F,F,T,F,T,T,F,T) = (F,T,F,T,T,F,T,F)) /\
  (GF256_by_2 (F,F,T,F,T,T,T,F) = (F,T,F,T,T,T,F,F)) /\
  (GF256_by_2 (F,F,T,F,T,T,T,T) = (F,T,F,T,T,T,T,F)) /\
  (GF256_by_2 (F,F,T,T,F,F,F,F) = (F,T,T,F,F,F,F,F)) /\
  (GF256_by_2 (F,F,T,T,F,F,F,T) = (F,T,T,F,F,F,T,F)) /\
  (GF256_by_2 (F,F,T,T,F,F,T,F) = (F,T,T,F,F,T,F,F)) /\
  (GF256_by_2 (F,F,T,T,F,F,T,T) = (F,T,T,F,F,T,T,F)) /\
  (GF256_by_2 (F,F,T,T,F,T,F,F) = (F,T,T,F,T,F,F,F)) /\
  (GF256_by_2 (F,F,T,T,F,T,F,T) = (F,T,T,F,T,F,T,F)) /\
  (GF256_by_2 (F,F,T,T,F,T,T,F) = (F,T,T,F,T,T,F,F)) /\
  (GF256_by_2 (F,F,T,T,F,T,T,T) = (F,T,T,F,T,T,T,F)) /\
  (GF256_by_2 (F,F,T,T,T,F,F,F) = (F,T,T,T,F,F,F,F)) /\
  (GF256_by_2 (F,F,T,T,T,F,F,T) = (F,T,T,T,F,F,T,F)) /\
  (GF256_by_2 (F,F,T,T,T,F,T,F) = (F,T,T,T,F,T,F,F)) /\
  (GF256_by_2 (F,F,T,T,T,F,T,T) = (F,T,T,T,F,T,T,F)) /\
  (GF256_by_2 (F,F,T,T,T,T,F,F) = (F,T,T,T,T,F,F,F)) /\
  (GF256_by_2 (F,F,T,T,T,T,F,T) = (F,T,T,T,T,F,T,F)) /\
  (GF256_by_2 (F,F,T,T,T,T,T,F) = (F,T,T,T,T,T,F,F)) /\
  (GF256_by_2 (F,F,T,T,T,T,T,T) = (F,T,T,T,T,T,T,F)) /\
  (GF256_by_2 (F,T,F,F,F,F,F,F) = (T,F,F,F,F,F,F,F)) /\
  (GF256_by_2 (F,T,F,F,F,F,F,T) = (T,F,F,F,F,F,T,F)) /\
  (GF256_by_2 (F,T,F,F,F,F,T,F) = (T,F,F,F,F,T,F,F)) /\
  (GF256_by_2 (F,T,F,F,F,F,T,T) = (T,F,F,F,F,T,T,F)) /\
  (GF256_by_2 (F,T,F,F,F,T,F,F) = (T,F,F,F,T,F,F,F)) /\
  (GF256_by_2 (F,T,F,F,F,T,F,T) = (T,F,F,F,T,F,T,F)) /\
  (GF256_by_2 (F,T,F,F,F,T,T,F) = (T,F,F,F,T,T,F,F)) /\
  (GF256_by_2 (F,T,F,F,F,T,T,T) = (T,F,F,F,T,T,T,F)) /\
  (GF256_by_2 (F,T,F,F,T,F,F,F) = (T,F,F,T,F,F,F,F)) /\
  (GF256_by_2 (F,T,F,F,T,F,F,T) = (T,F,F,T,F,F,T,F)) /\
  (GF256_by_2 (F,T,F,F,T,F,T,F) = (T,F,F,T,F,T,F,F)) /\
  (GF256_by_2 (F,T,F,F,T,F,T,T) = (T,F,F,T,F,T,T,F)) /\
  (GF256_by_2 (F,T,F,F,T,T,F,F) = (T,F,F,T,T,F,F,F)) /\
  (GF256_by_2 (F,T,F,F,T,T,F,T) = (T,F,F,T,T,F,T,F)) /\
  (GF256_by_2 (F,T,F,F,T,T,T,F) = (T,F,F,T,T,T,F,F)) /\
  (GF256_by_2 (F,T,F,F,T,T,T,T) = (T,F,F,T,T,T,T,F)) /\
  (GF256_by_2 (F,T,F,T,F,F,F,F) = (T,F,T,F,F,F,F,F)) /\
  (GF256_by_2 (F,T,F,T,F,F,F,T) = (T,F,T,F,F,F,T,F)) /\
  (GF256_by_2 (F,T,F,T,F,F,T,F) = (T,F,T,F,F,T,F,F)) /\
  (GF256_by_2 (F,T,F,T,F,F,T,T) = (T,F,T,F,F,T,T,F)) /\
  (GF256_by_2 (F,T,F,T,F,T,F,F) = (T,F,T,F,T,F,F,F)) /\
  (GF256_by_2 (F,T,F,T,F,T,F,T) = (T,F,T,F,T,F,T,F)) /\
  (GF256_by_2 (F,T,F,T,F,T,T,F) = (T,F,T,F,T,T,F,F)) /\
  (GF256_by_2 (F,T,F,T,F,T,T,T) = (T,F,T,F,T,T,T,F)) /\
  (GF256_by_2 (F,T,F,T,T,F,F,F) = (T,F,T,T,F,F,F,F)) /\
  (GF256_by_2 (F,T,F,T,T,F,F,T) = (T,F,T,T,F,F,T,F)) /\
  (GF256_by_2 (F,T,F,T,T,F,T,F) = (T,F,T,T,F,T,F,F)) /\
  (GF256_by_2 (F,T,F,T,T,F,T,T) = (T,F,T,T,F,T,T,F)) /\
  (GF256_by_2 (F,T,F,T,T,T,F,F) = (T,F,T,T,T,F,F,F)) /\
  (GF256_by_2 (F,T,F,T,T,T,F,T) = (T,F,T,T,T,F,T,F)) /\
  (GF256_by_2 (F,T,F,T,T,T,T,F) = (T,F,T,T,T,T,F,F)) /\
  (GF256_by_2 (F,T,F,T,T,T,T,T) = (T,F,T,T,T,T,T,F)) /\
  (GF256_by_2 (F,T,T,F,F,F,F,F) = (T,T,F,F,F,F,F,F)) /\
  (GF256_by_2 (F,T,T,F,F,F,F,T) = (T,T,F,F,F,F,T,F)) /\
  (GF256_by_2 (F,T,T,F,F,F,T,F) = (T,T,F,F,F,T,F,F)) /\
  (GF256_by_2 (F,T,T,F,F,F,T,T) = (T,T,F,F,F,T,T,F)) /\
  (GF256_by_2 (F,T,T,F,F,T,F,F) = (T,T,F,F,T,F,F,F)) /\
  (GF256_by_2 (F,T,T,F,F,T,F,T) = (T,T,F,F,T,F,T,F)) /\
  (GF256_by_2 (F,T,T,F,F,T,T,F) = (T,T,F,F,T,T,F,F)) /\
  (GF256_by_2 (F,T,T,F,F,T,T,T) = (T,T,F,F,T,T,T,F)) /\
  (GF256_by_2 (F,T,T,F,T,F,F,F) = (T,T,F,T,F,F,F,F)) /\
  (GF256_by_2 (F,T,T,F,T,F,F,T) = (T,T,F,T,F,F,T,F)) /\
  (GF256_by_2 (F,T,T,F,T,F,T,F) = (T,T,F,T,F,T,F,F)) /\
  (GF256_by_2 (F,T,T,F,T,F,T,T) = (T,T,F,T,F,T,T,F)) /\
  (GF256_by_2 (F,T,T,F,T,T,F,F) = (T,T,F,T,T,F,F,F)) /\
  (GF256_by_2 (F,T,T,F,T,T,F,T) = (T,T,F,T,T,F,T,F)) /\
  (GF256_by_2 (F,T,T,F,T,T,T,F) = (T,T,F,T,T,T,F,F)) /\
  (GF256_by_2 (F,T,T,F,T,T,T,T) = (T,T,F,T,T,T,T,F)) /\
  (GF256_by_2 (F,T,T,T,F,F,F,F) = (T,T,T,F,F,F,F,F)) /\
  (GF256_by_2 (F,T,T,T,F,F,F,T) = (T,T,T,F,F,F,T,F)) /\
  (GF256_by_2 (F,T,T,T,F,F,T,F) = (T,T,T,F,F,T,F,F)) /\
  (GF256_by_2 (F,T,T,T,F,F,T,T) = (T,T,T,F,F,T,T,F)) /\
  (GF256_by_2 (F,T,T,T,F,T,F,F) = (T,T,T,F,T,F,F,F)) /\
  (GF256_by_2 (F,T,T,T,F,T,F,T) = (T,T,T,F,T,F,T,F)) /\
  (GF256_by_2 (F,T,T,T,F,T,T,F) = (T,T,T,F,T,T,F,F)) /\
  (GF256_by_2 (F,T,T,T,F,T,T,T) = (T,T,T,F,T,T,T,F)) /\
  (GF256_by_2 (F,T,T,T,T,F,F,F) = (T,T,T,T,F,F,F,F)) /\
  (GF256_by_2 (F,T,T,T,T,F,F,T) = (T,T,T,T,F,F,T,F)) /\
  (GF256_by_2 (F,T,T,T,T,F,T,F) = (T,T,T,T,F,T,F,F)) /\
  (GF256_by_2 (F,T,T,T,T,F,T,T) = (T,T,T,T,F,T,T,F)) /\
  (GF256_by_2 (F,T,T,T,T,T,F,F) = (T,T,T,T,T,F,F,F)) /\
  (GF256_by_2 (F,T,T,T,T,T,F,T) = (T,T,T,T,T,F,T,F)) /\
  (GF256_by_2 (F,T,T,T,T,T,T,F) = (T,T,T,T,T,T,F,F)) /\
  (GF256_by_2 (F,T,T,T,T,T,T,T) = (T,T,T,T,T,T,T,F)) /\
  (GF256_by_2 (T,F,F,F,F,F,F,F) = (F,F,F,T,T,F,T,T)) /\
  (GF256_by_2 (T,F,F,F,F,F,F,T) = (F,F,F,T,T,F,F,T)) /\
  (GF256_by_2 (T,F,F,F,F,F,T,F) = (F,F,F,T,T,T,T,T)) /\
  (GF256_by_2 (T,F,F,F,F,F,T,T) = (F,F,F,T,T,T,F,T)) /\
  (GF256_by_2 (T,F,F,F,F,T,F,F) = (F,F,F,T,F,F,T,T)) /\
  (GF256_by_2 (T,F,F,F,F,T,F,T) = (F,F,F,T,F,F,F,T)) /\
  (GF256_by_2 (T,F,F,F,F,T,T,F) = (F,F,F,T,F,T,T,T)) /\
  (GF256_by_2 (T,F,F,F,F,T,T,T) = (F,F,F,T,F,T,F,T)) /\
  (GF256_by_2 (T,F,F,F,T,F,F,F) = (F,F,F,F,T,F,T,T)) /\
  (GF256_by_2 (T,F,F,F,T,F,F,T) = (F,F,F,F,T,F,F,T)) /\
  (GF256_by_2 (T,F,F,F,T,F,T,F) = (F,F,F,F,T,T,T,T)) /\
  (GF256_by_2 (T,F,F,F,T,F,T,T) = (F,F,F,F,T,T,F,T)) /\
  (GF256_by_2 (T,F,F,F,T,T,F,F) = (F,F,F,F,F,F,T,T)) /\
  (GF256_by_2 (T,F,F,F,T,T,F,T) = (F,F,F,F,F,F,F,T)) /\
  (GF256_by_2 (T,F,F,F,T,T,T,F) = (F,F,F,F,F,T,T,T)) /\
  (GF256_by_2 (T,F,F,F,T,T,T,T) = (F,F,F,F,F,T,F,T)) /\
  (GF256_by_2 (T,F,F,T,F,F,F,F) = (F,F,T,T,T,F,T,T)) /\
  (GF256_by_2 (T,F,F,T,F,F,F,T) = (F,F,T,T,T,F,F,T)) /\
  (GF256_by_2 (T,F,F,T,F,F,T,F) = (F,F,T,T,T,T,T,T)) /\
  (GF256_by_2 (T,F,F,T,F,F,T,T) = (F,F,T,T,T,T,F,T)) /\
  (GF256_by_2 (T,F,F,T,F,T,F,F) = (F,F,T,T,F,F,T,T)) /\
  (GF256_by_2 (T,F,F,T,F,T,F,T) = (F,F,T,T,F,F,F,T)) /\
  (GF256_by_2 (T,F,F,T,F,T,T,F) = (F,F,T,T,F,T,T,T)) /\
  (GF256_by_2 (T,F,F,T,F,T,T,T) = (F,F,T,T,F,T,F,T)) /\
  (GF256_by_2 (T,F,F,T,T,F,F,F) = (F,F,T,F,T,F,T,T)) /\
  (GF256_by_2 (T,F,F,T,T,F,F,T) = (F,F,T,F,T,F,F,T)) /\
  (GF256_by_2 (T,F,F,T,T,F,T,F) = (F,F,T,F,T,T,T,T)) /\
  (GF256_by_2 (T,F,F,T,T,F,T,T) = (F,F,T,F,T,T,F,T)) /\
  (GF256_by_2 (T,F,F,T,T,T,F,F) = (F,F,T,F,F,F,T,T)) /\
  (GF256_by_2 (T,F,F,T,T,T,F,T) = (F,F,T,F,F,F,F,T)) /\
  (GF256_by_2 (T,F,F,T,T,T,T,F) = (F,F,T,F,F,T,T,T)) /\
  (GF256_by_2 (T,F,F,T,T,T,T,T) = (F,F,T,F,F,T,F,T)) /\
  (GF256_by_2 (T,F,T,F,F,F,F,F) = (F,T,F,T,T,F,T,T)) /\
  (GF256_by_2 (T,F,T,F,F,F,F,T) = (F,T,F,T,T,F,F,T)) /\
  (GF256_by_2 (T,F,T,F,F,F,T,F) = (F,T,F,T,T,T,T,T)) /\
  (GF256_by_2 (T,F,T,F,F,F,T,T) = (F,T,F,T,T,T,F,T)) /\
  (GF256_by_2 (T,F,T,F,F,T,F,F) = (F,T,F,T,F,F,T,T)) /\
  (GF256_by_2 (T,F,T,F,F,T,F,T) = (F,T,F,T,F,F,F,T)) /\
  (GF256_by_2 (T,F,T,F,F,T,T,F) = (F,T,F,T,F,T,T,T)) /\
  (GF256_by_2 (T,F,T,F,F,T,T,T) = (F,T,F,T,F,T,F,T)) /\
  (GF256_by_2 (T,F,T,F,T,F,F,F) = (F,T,F,F,T,F,T,T)) /\
  (GF256_by_2 (T,F,T,F,T,F,F,T) = (F,T,F,F,T,F,F,T)) /\
  (GF256_by_2 (T,F,T,F,T,F,T,F) = (F,T,F,F,T,T,T,T)) /\
  (GF256_by_2 (T,F,T,F,T,F,T,T) = (F,T,F,F,T,T,F,T)) /\
  (GF256_by_2 (T,F,T,F,T,T,F,F) = (F,T,F,F,F,F,T,T)) /\
  (GF256_by_2 (T,F,T,F,T,T,F,T) = (F,T,F,F,F,F,F,T)) /\
  (GF256_by_2 (T,F,T,F,T,T,T,F) = (F,T,F,F,F,T,T,T)) /\
  (GF256_by_2 (T,F,T,F,T,T,T,T) = (F,T,F,F,F,T,F,T)) /\
  (GF256_by_2 (T,F,T,T,F,F,F,F) = (F,T,T,T,T,F,T,T)) /\
  (GF256_by_2 (T,F,T,T,F,F,F,T) = (F,T,T,T,T,F,F,T)) /\
  (GF256_by_2 (T,F,T,T,F,F,T,F) = (F,T,T,T,T,T,T,T)) /\
  (GF256_by_2 (T,F,T,T,F,F,T,T) = (F,T,T,T,T,T,F,T)) /\
  (GF256_by_2 (T,F,T,T,F,T,F,F) = (F,T,T,T,F,F,T,T)) /\
  (GF256_by_2 (T,F,T,T,F,T,F,T) = (F,T,T,T,F,F,F,T)) /\
  (GF256_by_2 (T,F,T,T,F,T,T,F) = (F,T,T,T,F,T,T,T)) /\
  (GF256_by_2 (T,F,T,T,F,T,T,T) = (F,T,T,T,F,T,F,T)) /\
  (GF256_by_2 (T,F,T,T,T,F,F,F) = (F,T,T,F,T,F,T,T)) /\
  (GF256_by_2 (T,F,T,T,T,F,F,T) = (F,T,T,F,T,F,F,T)) /\
  (GF256_by_2 (T,F,T,T,T,F,T,F) = (F,T,T,F,T,T,T,T)) /\
  (GF256_by_2 (T,F,T,T,T,F,T,T) = (F,T,T,F,T,T,F,T)) /\
  (GF256_by_2 (T,F,T,T,T,T,F,F) = (F,T,T,F,F,F,T,T)) /\
  (GF256_by_2 (T,F,T,T,T,T,F,T) = (F,T,T,F,F,F,F,T)) /\
  (GF256_by_2 (T,F,T,T,T,T,T,F) = (F,T,T,F,F,T,T,T)) /\
  (GF256_by_2 (T,F,T,T,T,T,T,T) = (F,T,T,F,F,T,F,T)) /\
  (GF256_by_2 (T,T,F,F,F,F,F,F) = (T,F,F,T,T,F,T,T)) /\
  (GF256_by_2 (T,T,F,F,F,F,F,T) = (T,F,F,T,T,F,F,T)) /\
  (GF256_by_2 (T,T,F,F,F,F,T,F) = (T,F,F,T,T,T,T,T)) /\
  (GF256_by_2 (T,T,F,F,F,F,T,T) = (T,F,F,T,T,T,F,T)) /\
  (GF256_by_2 (T,T,F,F,F,T,F,F) = (T,F,F,T,F,F,T,T)) /\
  (GF256_by_2 (T,T,F,F,F,T,F,T) = (T,F,F,T,F,F,F,T)) /\
  (GF256_by_2 (T,T,F,F,F,T,T,F) = (T,F,F,T,F,T,T,T)) /\
  (GF256_by_2 (T,T,F,F,F,T,T,T) = (T,F,F,T,F,T,F,T)) /\
  (GF256_by_2 (T,T,F,F,T,F,F,F) = (T,F,F,F,T,F,T,T)) /\
  (GF256_by_2 (T,T,F,F,T,F,F,T) = (T,F,F,F,T,F,F,T)) /\
  (GF256_by_2 (T,T,F,F,T,F,T,F) = (T,F,F,F,T,T,T,T)) /\
  (GF256_by_2 (T,T,F,F,T,F,T,T) = (T,F,F,F,T,T,F,T)) /\
  (GF256_by_2 (T,T,F,F,T,T,F,F) = (T,F,F,F,F,F,T,T)) /\
  (GF256_by_2 (T,T,F,F,T,T,F,T) = (T,F,F,F,F,F,F,T)) /\
  (GF256_by_2 (T,T,F,F,T,T,T,F) = (T,F,F,F,F,T,T,T)) /\
  (GF256_by_2 (T,T,F,F,T,T,T,T) = (T,F,F,F,F,T,F,T)) /\
  (GF256_by_2 (T,T,F,T,F,F,F,F) = (T,F,T,T,T,F,T,T)) /\
  (GF256_by_2 (T,T,F,T,F,F,F,T) = (T,F,T,T,T,F,F,T)) /\
  (GF256_by_2 (T,T,F,T,F,F,T,F) = (T,F,T,T,T,T,T,T)) /\
  (GF256_by_2 (T,T,F,T,F,F,T,T) = (T,F,T,T,T,T,F,T)) /\
  (GF256_by_2 (T,T,F,T,F,T,F,F) = (T,F,T,T,F,F,T,T)) /\
  (GF256_by_2 (T,T,F,T,F,T,F,T) = (T,F,T,T,F,F,F,T)) /\
  (GF256_by_2 (T,T,F,T,F,T,T,F) = (T,F,T,T,F,T,T,T)) /\
  (GF256_by_2 (T,T,F,T,F,T,T,T) = (T,F,T,T,F,T,F,T)) /\
  (GF256_by_2 (T,T,F,T,T,F,F,F) = (T,F,T,F,T,F,T,T)) /\
  (GF256_by_2 (T,T,F,T,T,F,F,T) = (T,F,T,F,T,F,F,T)) /\
  (GF256_by_2 (T,T,F,T,T,F,T,F) = (T,F,T,F,T,T,T,T)) /\
  (GF256_by_2 (T,T,F,T,T,F,T,T) = (T,F,T,F,T,T,F,T)) /\
  (GF256_by_2 (T,T,F,T,T,T,F,F) = (T,F,T,F,F,F,T,T)) /\
  (GF256_by_2 (T,T,F,T,T,T,F,T) = (T,F,T,F,F,F,F,T)) /\
  (GF256_by_2 (T,T,F,T,T,T,T,F) = (T,F,T,F,F,T,T,T)) /\
  (GF256_by_2 (T,T,F,T,T,T,T,T) = (T,F,T,F,F,T,F,T)) /\
  (GF256_by_2 (T,T,T,F,F,F,F,F) = (T,T,F,T,T,F,T,T)) /\
  (GF256_by_2 (T,T,T,F,F,F,F,T) = (T,T,F,T,T,F,F,T)) /\
  (GF256_by_2 (T,T,T,F,F,F,T,F) = (T,T,F,T,T,T,T,T)) /\
  (GF256_by_2 (T,T,T,F,F,F,T,T) = (T,T,F,T,T,T,F,T)) /\
  (GF256_by_2 (T,T,T,F,F,T,F,F) = (T,T,F,T,F,F,T,T)) /\
  (GF256_by_2 (T,T,T,F,F,T,F,T) = (T,T,F,T,F,F,F,T)) /\
  (GF256_by_2 (T,T,T,F,F,T,T,F) = (T,T,F,T,F,T,T,T)) /\
  (GF256_by_2 (T,T,T,F,F,T,T,T) = (T,T,F,T,F,T,F,T)) /\
  (GF256_by_2 (T,T,T,F,T,F,F,F) = (T,T,F,F,T,F,T,T)) /\
  (GF256_by_2 (T,T,T,F,T,F,F,T) = (T,T,F,F,T,F,F,T)) /\
  (GF256_by_2 (T,T,T,F,T,F,T,F) = (T,T,F,F,T,T,T,T)) /\
  (GF256_by_2 (T,T,T,F,T,F,T,T) = (T,T,F,F,T,T,F,T)) /\
  (GF256_by_2 (T,T,T,F,T,T,F,F) = (T,T,F,F,F,F,T,T)) /\
  (GF256_by_2 (T,T,T,F,T,T,F,T) = (T,T,F,F,F,F,F,T)) /\
  (GF256_by_2 (T,T,T,F,T,T,T,F) = (T,T,F,F,F,T,T,T)) /\
  (GF256_by_2 (T,T,T,F,T,T,T,T) = (T,T,F,F,F,T,F,T)) /\
  (GF256_by_2 (T,T,T,T,F,F,F,F) = (T,T,T,T,T,F,T,T)) /\
  (GF256_by_2 (T,T,T,T,F,F,F,T) = (T,T,T,T,T,F,F,T)) /\
  (GF256_by_2 (T,T,T,T,F,F,T,F) = (T,T,T,T,T,T,T,T)) /\
  (GF256_by_2 (T,T,T,T,F,F,T,T) = (T,T,T,T,T,T,F,T)) /\
  (GF256_by_2 (T,T,T,T,F,T,F,F) = (T,T,T,T,F,F,T,T)) /\
  (GF256_by_2 (T,T,T,T,F,T,F,T) = (T,T,T,T,F,F,F,T)) /\
  (GF256_by_2 (T,T,T,T,F,T,T,F) = (T,T,T,T,F,T,T,T)) /\
  (GF256_by_2 (T,T,T,T,F,T,T,T) = (T,T,T,T,F,T,F,T)) /\
  (GF256_by_2 (T,T,T,T,T,F,F,F) = (T,T,T,F,T,F,T,T)) /\
  (GF256_by_2 (T,T,T,T,T,F,F,T) = (T,T,T,F,T,F,F,T)) /\
  (GF256_by_2 (T,T,T,T,T,F,T,F) = (T,T,T,F,T,T,T,T)) /\
  (GF256_by_2 (T,T,T,T,T,F,T,T) = (T,T,T,F,T,T,F,T)) /\
  (GF256_by_2 (T,T,T,T,T,T,F,F) = (T,T,T,F,F,F,T,T)) /\
  (GF256_by_2 (T,T,T,T,T,T,F,T) = (T,T,T,F,F,F,F,T)) /\
  (GF256_by_2 (T,T,T,T,T,T,T,F) = (T,T,T,F,F,T,T,T)) /\
  (GF256_by_2 (T,T,T,T,T,T,T,T) = (T,T,T,F,F,T,F,T))`;

val GF256_by_3_def = Count.apply Define
 `(GF256_by_3 (F,F,F,F,F,F,F,F) = (F,F,F,F,F,F,F,F)) /\
  (GF256_by_3 (F,F,F,F,F,F,F,T) = (F,F,F,F,F,F,T,T)) /\
  (GF256_by_3 (F,F,F,F,F,F,T,F) = (F,F,F,F,F,T,T,F)) /\
  (GF256_by_3 (F,F,F,F,F,F,T,T) = (F,F,F,F,F,T,F,T)) /\
  (GF256_by_3 (F,F,F,F,F,T,F,F) = (F,F,F,F,T,T,F,F)) /\
  (GF256_by_3 (F,F,F,F,F,T,F,T) = (F,F,F,F,T,T,T,T)) /\
  (GF256_by_3 (F,F,F,F,F,T,T,F) = (F,F,F,F,T,F,T,F)) /\
  (GF256_by_3 (F,F,F,F,F,T,T,T) = (F,F,F,F,T,F,F,T)) /\
  (GF256_by_3 (F,F,F,F,T,F,F,F) = (F,F,F,T,T,F,F,F)) /\
  (GF256_by_3 (F,F,F,F,T,F,F,T) = (F,F,F,T,T,F,T,T)) /\
  (GF256_by_3 (F,F,F,F,T,F,T,F) = (F,F,F,T,T,T,T,F)) /\
  (GF256_by_3 (F,F,F,F,T,F,T,T) = (F,F,F,T,T,T,F,T)) /\
  (GF256_by_3 (F,F,F,F,T,T,F,F) = (F,F,F,T,F,T,F,F)) /\
  (GF256_by_3 (F,F,F,F,T,T,F,T) = (F,F,F,T,F,T,T,T)) /\
  (GF256_by_3 (F,F,F,F,T,T,T,F) = (F,F,F,T,F,F,T,F)) /\
  (GF256_by_3 (F,F,F,F,T,T,T,T) = (F,F,F,T,F,F,F,T)) /\
  (GF256_by_3 (F,F,F,T,F,F,F,F) = (F,F,T,T,F,F,F,F)) /\
  (GF256_by_3 (F,F,F,T,F,F,F,T) = (F,F,T,T,F,F,T,T)) /\
  (GF256_by_3 (F,F,F,T,F,F,T,F) = (F,F,T,T,F,T,T,F)) /\
  (GF256_by_3 (F,F,F,T,F,F,T,T) = (F,F,T,T,F,T,F,T)) /\
  (GF256_by_3 (F,F,F,T,F,T,F,F) = (F,F,T,T,T,T,F,F)) /\
  (GF256_by_3 (F,F,F,T,F,T,F,T) = (F,F,T,T,T,T,T,T)) /\
  (GF256_by_3 (F,F,F,T,F,T,T,F) = (F,F,T,T,T,F,T,F)) /\
  (GF256_by_3 (F,F,F,T,F,T,T,T) = (F,F,T,T,T,F,F,T)) /\
  (GF256_by_3 (F,F,F,T,T,F,F,F) = (F,F,T,F,T,F,F,F)) /\
  (GF256_by_3 (F,F,F,T,T,F,F,T) = (F,F,T,F,T,F,T,T)) /\
  (GF256_by_3 (F,F,F,T,T,F,T,F) = (F,F,T,F,T,T,T,F)) /\
  (GF256_by_3 (F,F,F,T,T,F,T,T) = (F,F,T,F,T,T,F,T)) /\
  (GF256_by_3 (F,F,F,T,T,T,F,F) = (F,F,T,F,F,T,F,F)) /\
  (GF256_by_3 (F,F,F,T,T,T,F,T) = (F,F,T,F,F,T,T,T)) /\
  (GF256_by_3 (F,F,F,T,T,T,T,F) = (F,F,T,F,F,F,T,F)) /\
  (GF256_by_3 (F,F,F,T,T,T,T,T) = (F,F,T,F,F,F,F,T)) /\
  (GF256_by_3 (F,F,T,F,F,F,F,F) = (F,T,T,F,F,F,F,F)) /\
  (GF256_by_3 (F,F,T,F,F,F,F,T) = (F,T,T,F,F,F,T,T)) /\
  (GF256_by_3 (F,F,T,F,F,F,T,F) = (F,T,T,F,F,T,T,F)) /\
  (GF256_by_3 (F,F,T,F,F,F,T,T) = (F,T,T,F,F,T,F,T)) /\
  (GF256_by_3 (F,F,T,F,F,T,F,F) = (F,T,T,F,T,T,F,F)) /\
  (GF256_by_3 (F,F,T,F,F,T,F,T) = (F,T,T,F,T,T,T,T)) /\
  (GF256_by_3 (F,F,T,F,F,T,T,F) = (F,T,T,F,T,F,T,F)) /\
  (GF256_by_3 (F,F,T,F,F,T,T,T) = (F,T,T,F,T,F,F,T)) /\
  (GF256_by_3 (F,F,T,F,T,F,F,F) = (F,T,T,T,T,F,F,F)) /\
  (GF256_by_3 (F,F,T,F,T,F,F,T) = (F,T,T,T,T,F,T,T)) /\
  (GF256_by_3 (F,F,T,F,T,F,T,F) = (F,T,T,T,T,T,T,F)) /\
  (GF256_by_3 (F,F,T,F,T,F,T,T) = (F,T,T,T,T,T,F,T)) /\
  (GF256_by_3 (F,F,T,F,T,T,F,F) = (F,T,T,T,F,T,F,F)) /\
  (GF256_by_3 (F,F,T,F,T,T,F,T) = (F,T,T,T,F,T,T,T)) /\
  (GF256_by_3 (F,F,T,F,T,T,T,F) = (F,T,T,T,F,F,T,F)) /\
  (GF256_by_3 (F,F,T,F,T,T,T,T) = (F,T,T,T,F,F,F,T)) /\
  (GF256_by_3 (F,F,T,T,F,F,F,F) = (F,T,F,T,F,F,F,F)) /\
  (GF256_by_3 (F,F,T,T,F,F,F,T) = (F,T,F,T,F,F,T,T)) /\
  (GF256_by_3 (F,F,T,T,F,F,T,F) = (F,T,F,T,F,T,T,F)) /\
  (GF256_by_3 (F,F,T,T,F,F,T,T) = (F,T,F,T,F,T,F,T)) /\
  (GF256_by_3 (F,F,T,T,F,T,F,F) = (F,T,F,T,T,T,F,F)) /\
  (GF256_by_3 (F,F,T,T,F,T,F,T) = (F,T,F,T,T,T,T,T)) /\
  (GF256_by_3 (F,F,T,T,F,T,T,F) = (F,T,F,T,T,F,T,F)) /\
  (GF256_by_3 (F,F,T,T,F,T,T,T) = (F,T,F,T,T,F,F,T)) /\
  (GF256_by_3 (F,F,T,T,T,F,F,F) = (F,T,F,F,T,F,F,F)) /\
  (GF256_by_3 (F,F,T,T,T,F,F,T) = (F,T,F,F,T,F,T,T)) /\
  (GF256_by_3 (F,F,T,T,T,F,T,F) = (F,T,F,F,T,T,T,F)) /\
  (GF256_by_3 (F,F,T,T,T,F,T,T) = (F,T,F,F,T,T,F,T)) /\
  (GF256_by_3 (F,F,T,T,T,T,F,F) = (F,T,F,F,F,T,F,F)) /\
  (GF256_by_3 (F,F,T,T,T,T,F,T) = (F,T,F,F,F,T,T,T)) /\
  (GF256_by_3 (F,F,T,T,T,T,T,F) = (F,T,F,F,F,F,T,F)) /\
  (GF256_by_3 (F,F,T,T,T,T,T,T) = (F,T,F,F,F,F,F,T)) /\
  (GF256_by_3 (F,T,F,F,F,F,F,F) = (T,T,F,F,F,F,F,F)) /\
  (GF256_by_3 (F,T,F,F,F,F,F,T) = (T,T,F,F,F,F,T,T)) /\
  (GF256_by_3 (F,T,F,F,F,F,T,F) = (T,T,F,F,F,T,T,F)) /\
  (GF256_by_3 (F,T,F,F,F,F,T,T) = (T,T,F,F,F,T,F,T)) /\
  (GF256_by_3 (F,T,F,F,F,T,F,F) = (T,T,F,F,T,T,F,F)) /\
  (GF256_by_3 (F,T,F,F,F,T,F,T) = (T,T,F,F,T,T,T,T)) /\
  (GF256_by_3 (F,T,F,F,F,T,T,F) = (T,T,F,F,T,F,T,F)) /\
  (GF256_by_3 (F,T,F,F,F,T,T,T) = (T,T,F,F,T,F,F,T)) /\
  (GF256_by_3 (F,T,F,F,T,F,F,F) = (T,T,F,T,T,F,F,F)) /\
  (GF256_by_3 (F,T,F,F,T,F,F,T) = (T,T,F,T,T,F,T,T)) /\
  (GF256_by_3 (F,T,F,F,T,F,T,F) = (T,T,F,T,T,T,T,F)) /\
  (GF256_by_3 (F,T,F,F,T,F,T,T) = (T,T,F,T,T,T,F,T)) /\
  (GF256_by_3 (F,T,F,F,T,T,F,F) = (T,T,F,T,F,T,F,F)) /\
  (GF256_by_3 (F,T,F,F,T,T,F,T) = (T,T,F,T,F,T,T,T)) /\
  (GF256_by_3 (F,T,F,F,T,T,T,F) = (T,T,F,T,F,F,T,F)) /\
  (GF256_by_3 (F,T,F,F,T,T,T,T) = (T,T,F,T,F,F,F,T)) /\
  (GF256_by_3 (F,T,F,T,F,F,F,F) = (T,T,T,T,F,F,F,F)) /\
  (GF256_by_3 (F,T,F,T,F,F,F,T) = (T,T,T,T,F,F,T,T)) /\
  (GF256_by_3 (F,T,F,T,F,F,T,F) = (T,T,T,T,F,T,T,F)) /\
  (GF256_by_3 (F,T,F,T,F,F,T,T) = (T,T,T,T,F,T,F,T)) /\
  (GF256_by_3 (F,T,F,T,F,T,F,F) = (T,T,T,T,T,T,F,F)) /\
  (GF256_by_3 (F,T,F,T,F,T,F,T) = (T,T,T,T,T,T,T,T)) /\
  (GF256_by_3 (F,T,F,T,F,T,T,F) = (T,T,T,T,T,F,T,F)) /\
  (GF256_by_3 (F,T,F,T,F,T,T,T) = (T,T,T,T,T,F,F,T)) /\
  (GF256_by_3 (F,T,F,T,T,F,F,F) = (T,T,T,F,T,F,F,F)) /\
  (GF256_by_3 (F,T,F,T,T,F,F,T) = (T,T,T,F,T,F,T,T)) /\
  (GF256_by_3 (F,T,F,T,T,F,T,F) = (T,T,T,F,T,T,T,F)) /\
  (GF256_by_3 (F,T,F,T,T,F,T,T) = (T,T,T,F,T,T,F,T)) /\
  (GF256_by_3 (F,T,F,T,T,T,F,F) = (T,T,T,F,F,T,F,F)) /\
  (GF256_by_3 (F,T,F,T,T,T,F,T) = (T,T,T,F,F,T,T,T)) /\
  (GF256_by_3 (F,T,F,T,T,T,T,F) = (T,T,T,F,F,F,T,F)) /\
  (GF256_by_3 (F,T,F,T,T,T,T,T) = (T,T,T,F,F,F,F,T)) /\
  (GF256_by_3 (F,T,T,F,F,F,F,F) = (T,F,T,F,F,F,F,F)) /\
  (GF256_by_3 (F,T,T,F,F,F,F,T) = (T,F,T,F,F,F,T,T)) /\
  (GF256_by_3 (F,T,T,F,F,F,T,F) = (T,F,T,F,F,T,T,F)) /\
  (GF256_by_3 (F,T,T,F,F,F,T,T) = (T,F,T,F,F,T,F,T)) /\
  (GF256_by_3 (F,T,T,F,F,T,F,F) = (T,F,T,F,T,T,F,F)) /\
  (GF256_by_3 (F,T,T,F,F,T,F,T) = (T,F,T,F,T,T,T,T)) /\
  (GF256_by_3 (F,T,T,F,F,T,T,F) = (T,F,T,F,T,F,T,F)) /\
  (GF256_by_3 (F,T,T,F,F,T,T,T) = (T,F,T,F,T,F,F,T)) /\
  (GF256_by_3 (F,T,T,F,T,F,F,F) = (T,F,T,T,T,F,F,F)) /\
  (GF256_by_3 (F,T,T,F,T,F,F,T) = (T,F,T,T,T,F,T,T)) /\
  (GF256_by_3 (F,T,T,F,T,F,T,F) = (T,F,T,T,T,T,T,F)) /\
  (GF256_by_3 (F,T,T,F,T,F,T,T) = (T,F,T,T,T,T,F,T)) /\
  (GF256_by_3 (F,T,T,F,T,T,F,F) = (T,F,T,T,F,T,F,F)) /\
  (GF256_by_3 (F,T,T,F,T,T,F,T) = (T,F,T,T,F,T,T,T)) /\
  (GF256_by_3 (F,T,T,F,T,T,T,F) = (T,F,T,T,F,F,T,F)) /\
  (GF256_by_3 (F,T,T,F,T,T,T,T) = (T,F,T,T,F,F,F,T)) /\
  (GF256_by_3 (F,T,T,T,F,F,F,F) = (T,F,F,T,F,F,F,F)) /\
  (GF256_by_3 (F,T,T,T,F,F,F,T) = (T,F,F,T,F,F,T,T)) /\
  (GF256_by_3 (F,T,T,T,F,F,T,F) = (T,F,F,T,F,T,T,F)) /\
  (GF256_by_3 (F,T,T,T,F,F,T,T) = (T,F,F,T,F,T,F,T)) /\
  (GF256_by_3 (F,T,T,T,F,T,F,F) = (T,F,F,T,T,T,F,F)) /\
  (GF256_by_3 (F,T,T,T,F,T,F,T) = (T,F,F,T,T,T,T,T)) /\
  (GF256_by_3 (F,T,T,T,F,T,T,F) = (T,F,F,T,T,F,T,F)) /\
  (GF256_by_3 (F,T,T,T,F,T,T,T) = (T,F,F,T,T,F,F,T)) /\
  (GF256_by_3 (F,T,T,T,T,F,F,F) = (T,F,F,F,T,F,F,F)) /\
  (GF256_by_3 (F,T,T,T,T,F,F,T) = (T,F,F,F,T,F,T,T)) /\
  (GF256_by_3 (F,T,T,T,T,F,T,F) = (T,F,F,F,T,T,T,F)) /\
  (GF256_by_3 (F,T,T,T,T,F,T,T) = (T,F,F,F,T,T,F,T)) /\
  (GF256_by_3 (F,T,T,T,T,T,F,F) = (T,F,F,F,F,T,F,F)) /\
  (GF256_by_3 (F,T,T,T,T,T,F,T) = (T,F,F,F,F,T,T,T)) /\
  (GF256_by_3 (F,T,T,T,T,T,T,F) = (T,F,F,F,F,F,T,F)) /\
  (GF256_by_3 (F,T,T,T,T,T,T,T) = (T,F,F,F,F,F,F,T)) /\
  (GF256_by_3 (T,F,F,F,F,F,F,F) = (T,F,F,T,T,F,T,T)) /\
  (GF256_by_3 (T,F,F,F,F,F,F,T) = (T,F,F,T,T,F,F,F)) /\
  (GF256_by_3 (T,F,F,F,F,F,T,F) = (T,F,F,T,T,T,F,T)) /\
  (GF256_by_3 (T,F,F,F,F,F,T,T) = (T,F,F,T,T,T,T,F)) /\
  (GF256_by_3 (T,F,F,F,F,T,F,F) = (T,F,F,T,F,T,T,T)) /\
  (GF256_by_3 (T,F,F,F,F,T,F,T) = (T,F,F,T,F,T,F,F)) /\
  (GF256_by_3 (T,F,F,F,F,T,T,F) = (T,F,F,T,F,F,F,T)) /\
  (GF256_by_3 (T,F,F,F,F,T,T,T) = (T,F,F,T,F,F,T,F)) /\
  (GF256_by_3 (T,F,F,F,T,F,F,F) = (T,F,F,F,F,F,T,T)) /\
  (GF256_by_3 (T,F,F,F,T,F,F,T) = (T,F,F,F,F,F,F,F)) /\
  (GF256_by_3 (T,F,F,F,T,F,T,F) = (T,F,F,F,F,T,F,T)) /\
  (GF256_by_3 (T,F,F,F,T,F,T,T) = (T,F,F,F,F,T,T,F)) /\
  (GF256_by_3 (T,F,F,F,T,T,F,F) = (T,F,F,F,T,T,T,T)) /\
  (GF256_by_3 (T,F,F,F,T,T,F,T) = (T,F,F,F,T,T,F,F)) /\
  (GF256_by_3 (T,F,F,F,T,T,T,F) = (T,F,F,F,T,F,F,T)) /\
  (GF256_by_3 (T,F,F,F,T,T,T,T) = (T,F,F,F,T,F,T,F)) /\
  (GF256_by_3 (T,F,F,T,F,F,F,F) = (T,F,T,F,T,F,T,T)) /\
  (GF256_by_3 (T,F,F,T,F,F,F,T) = (T,F,T,F,T,F,F,F)) /\
  (GF256_by_3 (T,F,F,T,F,F,T,F) = (T,F,T,F,T,T,F,T)) /\
  (GF256_by_3 (T,F,F,T,F,F,T,T) = (T,F,T,F,T,T,T,F)) /\
  (GF256_by_3 (T,F,F,T,F,T,F,F) = (T,F,T,F,F,T,T,T)) /\
  (GF256_by_3 (T,F,F,T,F,T,F,T) = (T,F,T,F,F,T,F,F)) /\
  (GF256_by_3 (T,F,F,T,F,T,T,F) = (T,F,T,F,F,F,F,T)) /\
  (GF256_by_3 (T,F,F,T,F,T,T,T) = (T,F,T,F,F,F,T,F)) /\
  (GF256_by_3 (T,F,F,T,T,F,F,F) = (T,F,T,T,F,F,T,T)) /\
  (GF256_by_3 (T,F,F,T,T,F,F,T) = (T,F,T,T,F,F,F,F)) /\
  (GF256_by_3 (T,F,F,T,T,F,T,F) = (T,F,T,T,F,T,F,T)) /\
  (GF256_by_3 (T,F,F,T,T,F,T,T) = (T,F,T,T,F,T,T,F)) /\
  (GF256_by_3 (T,F,F,T,T,T,F,F) = (T,F,T,T,T,T,T,T)) /\
  (GF256_by_3 (T,F,F,T,T,T,F,T) = (T,F,T,T,T,T,F,F)) /\
  (GF256_by_3 (T,F,F,T,T,T,T,F) = (T,F,T,T,T,F,F,T)) /\
  (GF256_by_3 (T,F,F,T,T,T,T,T) = (T,F,T,T,T,F,T,F)) /\
  (GF256_by_3 (T,F,T,F,F,F,F,F) = (T,T,T,T,T,F,T,T)) /\
  (GF256_by_3 (T,F,T,F,F,F,F,T) = (T,T,T,T,T,F,F,F)) /\
  (GF256_by_3 (T,F,T,F,F,F,T,F) = (T,T,T,T,T,T,F,T)) /\
  (GF256_by_3 (T,F,T,F,F,F,T,T) = (T,T,T,T,T,T,T,F)) /\
  (GF256_by_3 (T,F,T,F,F,T,F,F) = (T,T,T,T,F,T,T,T)) /\
  (GF256_by_3 (T,F,T,F,F,T,F,T) = (T,T,T,T,F,T,F,F)) /\
  (GF256_by_3 (T,F,T,F,F,T,T,F) = (T,T,T,T,F,F,F,T)) /\
  (GF256_by_3 (T,F,T,F,F,T,T,T) = (T,T,T,T,F,F,T,F)) /\
  (GF256_by_3 (T,F,T,F,T,F,F,F) = (T,T,T,F,F,F,T,T)) /\
  (GF256_by_3 (T,F,T,F,T,F,F,T) = (T,T,T,F,F,F,F,F)) /\
  (GF256_by_3 (T,F,T,F,T,F,T,F) = (T,T,T,F,F,T,F,T)) /\
  (GF256_by_3 (T,F,T,F,T,F,T,T) = (T,T,T,F,F,T,T,F)) /\
  (GF256_by_3 (T,F,T,F,T,T,F,F) = (T,T,T,F,T,T,T,T)) /\
  (GF256_by_3 (T,F,T,F,T,T,F,T) = (T,T,T,F,T,T,F,F)) /\
  (GF256_by_3 (T,F,T,F,T,T,T,F) = (T,T,T,F,T,F,F,T)) /\
  (GF256_by_3 (T,F,T,F,T,T,T,T) = (T,T,T,F,T,F,T,F)) /\
  (GF256_by_3 (T,F,T,T,F,F,F,F) = (T,T,F,F,T,F,T,T)) /\
  (GF256_by_3 (T,F,T,T,F,F,F,T) = (T,T,F,F,T,F,F,F)) /\
  (GF256_by_3 (T,F,T,T,F,F,T,F) = (T,T,F,F,T,T,F,T)) /\
  (GF256_by_3 (T,F,T,T,F,F,T,T) = (T,T,F,F,T,T,T,F)) /\
  (GF256_by_3 (T,F,T,T,F,T,F,F) = (T,T,F,F,F,T,T,T)) /\
  (GF256_by_3 (T,F,T,T,F,T,F,T) = (T,T,F,F,F,T,F,F)) /\
  (GF256_by_3 (T,F,T,T,F,T,T,F) = (T,T,F,F,F,F,F,T)) /\
  (GF256_by_3 (T,F,T,T,F,T,T,T) = (T,T,F,F,F,F,T,F)) /\
  (GF256_by_3 (T,F,T,T,T,F,F,F) = (T,T,F,T,F,F,T,T)) /\
  (GF256_by_3 (T,F,T,T,T,F,F,T) = (T,T,F,T,F,F,F,F)) /\
  (GF256_by_3 (T,F,T,T,T,F,T,F) = (T,T,F,T,F,T,F,T)) /\
  (GF256_by_3 (T,F,T,T,T,F,T,T) = (T,T,F,T,F,T,T,F)) /\
  (GF256_by_3 (T,F,T,T,T,T,F,F) = (T,T,F,T,T,T,T,T)) /\
  (GF256_by_3 (T,F,T,T,T,T,F,T) = (T,T,F,T,T,T,F,F)) /\
  (GF256_by_3 (T,F,T,T,T,T,T,F) = (T,T,F,T,T,F,F,T)) /\
  (GF256_by_3 (T,F,T,T,T,T,T,T) = (T,T,F,T,T,F,T,F)) /\
  (GF256_by_3 (T,T,F,F,F,F,F,F) = (F,T,F,T,T,F,T,T)) /\
  (GF256_by_3 (T,T,F,F,F,F,F,T) = (F,T,F,T,T,F,F,F)) /\
  (GF256_by_3 (T,T,F,F,F,F,T,F) = (F,T,F,T,T,T,F,T)) /\
  (GF256_by_3 (T,T,F,F,F,F,T,T) = (F,T,F,T,T,T,T,F)) /\
  (GF256_by_3 (T,T,F,F,F,T,F,F) = (F,T,F,T,F,T,T,T)) /\
  (GF256_by_3 (T,T,F,F,F,T,F,T) = (F,T,F,T,F,T,F,F)) /\
  (GF256_by_3 (T,T,F,F,F,T,T,F) = (F,T,F,T,F,F,F,T)) /\
  (GF256_by_3 (T,T,F,F,F,T,T,T) = (F,T,F,T,F,F,T,F)) /\
  (GF256_by_3 (T,T,F,F,T,F,F,F) = (F,T,F,F,F,F,T,T)) /\
  (GF256_by_3 (T,T,F,F,T,F,F,T) = (F,T,F,F,F,F,F,F)) /\
  (GF256_by_3 (T,T,F,F,T,F,T,F) = (F,T,F,F,F,T,F,T)) /\
  (GF256_by_3 (T,T,F,F,T,F,T,T) = (F,T,F,F,F,T,T,F)) /\
  (GF256_by_3 (T,T,F,F,T,T,F,F) = (F,T,F,F,T,T,T,T)) /\
  (GF256_by_3 (T,T,F,F,T,T,F,T) = (F,T,F,F,T,T,F,F)) /\
  (GF256_by_3 (T,T,F,F,T,T,T,F) = (F,T,F,F,T,F,F,T)) /\
  (GF256_by_3 (T,T,F,F,T,T,T,T) = (F,T,F,F,T,F,T,F)) /\
  (GF256_by_3 (T,T,F,T,F,F,F,F) = (F,T,T,F,T,F,T,T)) /\
  (GF256_by_3 (T,T,F,T,F,F,F,T) = (F,T,T,F,T,F,F,F)) /\
  (GF256_by_3 (T,T,F,T,F,F,T,F) = (F,T,T,F,T,T,F,T)) /\
  (GF256_by_3 (T,T,F,T,F,F,T,T) = (F,T,T,F,T,T,T,F)) /\
  (GF256_by_3 (T,T,F,T,F,T,F,F) = (F,T,T,F,F,T,T,T)) /\
  (GF256_by_3 (T,T,F,T,F,T,F,T) = (F,T,T,F,F,T,F,F)) /\
  (GF256_by_3 (T,T,F,T,F,T,T,F) = (F,T,T,F,F,F,F,T)) /\
  (GF256_by_3 (T,T,F,T,F,T,T,T) = (F,T,T,F,F,F,T,F)) /\
  (GF256_by_3 (T,T,F,T,T,F,F,F) = (F,T,T,T,F,F,T,T)) /\
  (GF256_by_3 (T,T,F,T,T,F,F,T) = (F,T,T,T,F,F,F,F)) /\
  (GF256_by_3 (T,T,F,T,T,F,T,F) = (F,T,T,T,F,T,F,T)) /\
  (GF256_by_3 (T,T,F,T,T,F,T,T) = (F,T,T,T,F,T,T,F)) /\
  (GF256_by_3 (T,T,F,T,T,T,F,F) = (F,T,T,T,T,T,T,T)) /\
  (GF256_by_3 (T,T,F,T,T,T,F,T) = (F,T,T,T,T,T,F,F)) /\
  (GF256_by_3 (T,T,F,T,T,T,T,F) = (F,T,T,T,T,F,F,T)) /\
  (GF256_by_3 (T,T,F,T,T,T,T,T) = (F,T,T,T,T,F,T,F)) /\
  (GF256_by_3 (T,T,T,F,F,F,F,F) = (F,F,T,T,T,F,T,T)) /\
  (GF256_by_3 (T,T,T,F,F,F,F,T) = (F,F,T,T,T,F,F,F)) /\
  (GF256_by_3 (T,T,T,F,F,F,T,F) = (F,F,T,T,T,T,F,T)) /\
  (GF256_by_3 (T,T,T,F,F,F,T,T) = (F,F,T,T,T,T,T,F)) /\
  (GF256_by_3 (T,T,T,F,F,T,F,F) = (F,F,T,T,F,T,T,T)) /\
  (GF256_by_3 (T,T,T,F,F,T,F,T) = (F,F,T,T,F,T,F,F)) /\
  (GF256_by_3 (T,T,T,F,F,T,T,F) = (F,F,T,T,F,F,F,T)) /\
  (GF256_by_3 (T,T,T,F,F,T,T,T) = (F,F,T,T,F,F,T,F)) /\
  (GF256_by_3 (T,T,T,F,T,F,F,F) = (F,F,T,F,F,F,T,T)) /\
  (GF256_by_3 (T,T,T,F,T,F,F,T) = (F,F,T,F,F,F,F,F)) /\
  (GF256_by_3 (T,T,T,F,T,F,T,F) = (F,F,T,F,F,T,F,T)) /\
  (GF256_by_3 (T,T,T,F,T,F,T,T) = (F,F,T,F,F,T,T,F)) /\
  (GF256_by_3 (T,T,T,F,T,T,F,F) = (F,F,T,F,T,T,T,T)) /\
  (GF256_by_3 (T,T,T,F,T,T,F,T) = (F,F,T,F,T,T,F,F)) /\
  (GF256_by_3 (T,T,T,F,T,T,T,F) = (F,F,T,F,T,F,F,T)) /\
  (GF256_by_3 (T,T,T,F,T,T,T,T) = (F,F,T,F,T,F,T,F)) /\
  (GF256_by_3 (T,T,T,T,F,F,F,F) = (F,F,F,F,T,F,T,T)) /\
  (GF256_by_3 (T,T,T,T,F,F,F,T) = (F,F,F,F,T,F,F,F)) /\
  (GF256_by_3 (T,T,T,T,F,F,T,F) = (F,F,F,F,T,T,F,T)) /\
  (GF256_by_3 (T,T,T,T,F,F,T,T) = (F,F,F,F,T,T,T,F)) /\
  (GF256_by_3 (T,T,T,T,F,T,F,F) = (F,F,F,F,F,T,T,T)) /\
  (GF256_by_3 (T,T,T,T,F,T,F,T) = (F,F,F,F,F,T,F,F)) /\
  (GF256_by_3 (T,T,T,T,F,T,T,F) = (F,F,F,F,F,F,F,T)) /\
  (GF256_by_3 (T,T,T,T,F,T,T,T) = (F,F,F,F,F,F,T,F)) /\
  (GF256_by_3 (T,T,T,T,T,F,F,F) = (F,F,F,T,F,F,T,T)) /\
  (GF256_by_3 (T,T,T,T,T,F,F,T) = (F,F,F,T,F,F,F,F)) /\
  (GF256_by_3 (T,T,T,T,T,F,T,F) = (F,F,F,T,F,T,F,T)) /\
  (GF256_by_3 (T,T,T,T,T,F,T,T) = (F,F,F,T,F,T,T,F)) /\
  (GF256_by_3 (T,T,T,T,T,T,F,F) = (F,F,F,T,T,T,T,T)) /\
  (GF256_by_3 (T,T,T,T,T,T,F,T) = (F,F,F,T,T,T,F,F)) /\
  (GF256_by_3 (T,T,T,T,T,T,T,F) = (F,F,F,T,T,F,F,T)) /\
  (GF256_by_3 (T,T,T,T,T,T,T,T) = (F,F,F,T,T,F,T,F))`;

val GF256_by_9_def_def = Count.apply Define
 `(GF256_by_9 (F,F,F,F,F,F,F,F) = (F,F,F,F,F,F,F,F)) /\
  (GF256_by_9 (F,F,F,F,F,F,F,T) = (F,F,F,F,T,F,F,T)) /\
  (GF256_by_9 (F,F,F,F,F,F,T,F) = (F,F,F,T,F,F,T,F)) /\
  (GF256_by_9 (F,F,F,F,F,F,T,T) = (F,F,F,T,T,F,T,T)) /\
  (GF256_by_9 (F,F,F,F,F,T,F,F) = (F,F,T,F,F,T,F,F)) /\
  (GF256_by_9 (F,F,F,F,F,T,F,T) = (F,F,T,F,T,T,F,T)) /\
  (GF256_by_9 (F,F,F,F,F,T,T,F) = (F,F,T,T,F,T,T,F)) /\
  (GF256_by_9 (F,F,F,F,F,T,T,T) = (F,F,T,T,T,T,T,T)) /\
  (GF256_by_9 (F,F,F,F,T,F,F,F) = (F,T,F,F,T,F,F,F)) /\
  (GF256_by_9 (F,F,F,F,T,F,F,T) = (F,T,F,F,F,F,F,T)) /\
  (GF256_by_9 (F,F,F,F,T,F,T,F) = (F,T,F,T,T,F,T,F)) /\
  (GF256_by_9 (F,F,F,F,T,F,T,T) = (F,T,F,T,F,F,T,T)) /\
  (GF256_by_9 (F,F,F,F,T,T,F,F) = (F,T,T,F,T,T,F,F)) /\
  (GF256_by_9 (F,F,F,F,T,T,F,T) = (F,T,T,F,F,T,F,T)) /\
  (GF256_by_9 (F,F,F,F,T,T,T,F) = (F,T,T,T,T,T,T,F)) /\
  (GF256_by_9 (F,F,F,F,T,T,T,T) = (F,T,T,T,F,T,T,T)) /\
  (GF256_by_9 (F,F,F,T,F,F,F,F) = (T,F,F,T,F,F,F,F)) /\
  (GF256_by_9 (F,F,F,T,F,F,F,T) = (T,F,F,T,T,F,F,T)) /\
  (GF256_by_9 (F,F,F,T,F,F,T,F) = (T,F,F,F,F,F,T,F)) /\
  (GF256_by_9 (F,F,F,T,F,F,T,T) = (T,F,F,F,T,F,T,T)) /\
  (GF256_by_9 (F,F,F,T,F,T,F,F) = (T,F,T,T,F,T,F,F)) /\
  (GF256_by_9 (F,F,F,T,F,T,F,T) = (T,F,T,T,T,T,F,T)) /\
  (GF256_by_9 (F,F,F,T,F,T,T,F) = (T,F,T,F,F,T,T,F)) /\
  (GF256_by_9 (F,F,F,T,F,T,T,T) = (T,F,T,F,T,T,T,T)) /\
  (GF256_by_9 (F,F,F,T,T,F,F,F) = (T,T,F,T,T,F,F,F)) /\
  (GF256_by_9 (F,F,F,T,T,F,F,T) = (T,T,F,T,F,F,F,T)) /\
  (GF256_by_9 (F,F,F,T,T,F,T,F) = (T,T,F,F,T,F,T,F)) /\
  (GF256_by_9 (F,F,F,T,T,F,T,T) = (T,T,F,F,F,F,T,T)) /\
  (GF256_by_9 (F,F,F,T,T,T,F,F) = (T,T,T,T,T,T,F,F)) /\
  (GF256_by_9 (F,F,F,T,T,T,F,T) = (T,T,T,T,F,T,F,T)) /\
  (GF256_by_9 (F,F,F,T,T,T,T,F) = (T,T,T,F,T,T,T,F)) /\
  (GF256_by_9 (F,F,F,T,T,T,T,T) = (T,T,T,F,F,T,T,T)) /\
  (GF256_by_9 (F,F,T,F,F,F,F,F) = (F,F,T,T,T,F,T,T)) /\
  (GF256_by_9 (F,F,T,F,F,F,F,T) = (F,F,T,T,F,F,T,F)) /\
  (GF256_by_9 (F,F,T,F,F,F,T,F) = (F,F,T,F,T,F,F,T)) /\
  (GF256_by_9 (F,F,T,F,F,F,T,T) = (F,F,T,F,F,F,F,F)) /\
  (GF256_by_9 (F,F,T,F,F,T,F,F) = (F,F,F,T,T,T,T,T)) /\
  (GF256_by_9 (F,F,T,F,F,T,F,T) = (F,F,F,T,F,T,T,F)) /\
  (GF256_by_9 (F,F,T,F,F,T,T,F) = (F,F,F,F,T,T,F,T)) /\
  (GF256_by_9 (F,F,T,F,F,T,T,T) = (F,F,F,F,F,T,F,F)) /\
  (GF256_by_9 (F,F,T,F,T,F,F,F) = (F,T,T,T,F,F,T,T)) /\
  (GF256_by_9 (F,F,T,F,T,F,F,T) = (F,T,T,T,T,F,T,F)) /\
  (GF256_by_9 (F,F,T,F,T,F,T,F) = (F,T,T,F,F,F,F,T)) /\
  (GF256_by_9 (F,F,T,F,T,F,T,T) = (F,T,T,F,T,F,F,F)) /\
  (GF256_by_9 (F,F,T,F,T,T,F,F) = (F,T,F,T,F,T,T,T)) /\
  (GF256_by_9 (F,F,T,F,T,T,F,T) = (F,T,F,T,T,T,T,F)) /\
  (GF256_by_9 (F,F,T,F,T,T,T,F) = (F,T,F,F,F,T,F,T)) /\
  (GF256_by_9 (F,F,T,F,T,T,T,T) = (F,T,F,F,T,T,F,F)) /\
  (GF256_by_9 (F,F,T,T,F,F,F,F) = (T,F,T,F,T,F,T,T)) /\
  (GF256_by_9 (F,F,T,T,F,F,F,T) = (T,F,T,F,F,F,T,F)) /\
  (GF256_by_9 (F,F,T,T,F,F,T,F) = (T,F,T,T,T,F,F,T)) /\
  (GF256_by_9 (F,F,T,T,F,F,T,T) = (T,F,T,T,F,F,F,F)) /\
  (GF256_by_9 (F,F,T,T,F,T,F,F) = (T,F,F,F,T,T,T,T)) /\
  (GF256_by_9 (F,F,T,T,F,T,F,T) = (T,F,F,F,F,T,T,F)) /\
  (GF256_by_9 (F,F,T,T,F,T,T,F) = (T,F,F,T,T,T,F,T)) /\
  (GF256_by_9 (F,F,T,T,F,T,T,T) = (T,F,F,T,F,T,F,F)) /\
  (GF256_by_9 (F,F,T,T,T,F,F,F) = (T,T,T,F,F,F,T,T)) /\
  (GF256_by_9 (F,F,T,T,T,F,F,T) = (T,T,T,F,T,F,T,F)) /\
  (GF256_by_9 (F,F,T,T,T,F,T,F) = (T,T,T,T,F,F,F,T)) /\
  (GF256_by_9 (F,F,T,T,T,F,T,T) = (T,T,T,T,T,F,F,F)) /\
  (GF256_by_9 (F,F,T,T,T,T,F,F) = (T,T,F,F,F,T,T,T)) /\
  (GF256_by_9 (F,F,T,T,T,T,F,T) = (T,T,F,F,T,T,T,F)) /\
  (GF256_by_9 (F,F,T,T,T,T,T,F) = (T,T,F,T,F,T,F,T)) /\
  (GF256_by_9 (F,F,T,T,T,T,T,T) = (T,T,F,T,T,T,F,F)) /\
  (GF256_by_9 (F,T,F,F,F,F,F,F) = (F,T,T,T,F,T,T,F)) /\
  (GF256_by_9 (F,T,F,F,F,F,F,T) = (F,T,T,T,T,T,T,T)) /\
  (GF256_by_9 (F,T,F,F,F,F,T,F) = (F,T,T,F,F,T,F,F)) /\
  (GF256_by_9 (F,T,F,F,F,F,T,T) = (F,T,T,F,T,T,F,T)) /\
  (GF256_by_9 (F,T,F,F,F,T,F,F) = (F,T,F,T,F,F,T,F)) /\
  (GF256_by_9 (F,T,F,F,F,T,F,T) = (F,T,F,T,T,F,T,T)) /\
  (GF256_by_9 (F,T,F,F,F,T,T,F) = (F,T,F,F,F,F,F,F)) /\
  (GF256_by_9 (F,T,F,F,F,T,T,T) = (F,T,F,F,T,F,F,T)) /\
  (GF256_by_9 (F,T,F,F,T,F,F,F) = (F,F,T,T,T,T,T,F)) /\
  (GF256_by_9 (F,T,F,F,T,F,F,T) = (F,F,T,T,F,T,T,T)) /\
  (GF256_by_9 (F,T,F,F,T,F,T,F) = (F,F,T,F,T,T,F,F)) /\
  (GF256_by_9 (F,T,F,F,T,F,T,T) = (F,F,T,F,F,T,F,T)) /\
  (GF256_by_9 (F,T,F,F,T,T,F,F) = (F,F,F,T,T,F,T,F)) /\
  (GF256_by_9 (F,T,F,F,T,T,F,T) = (F,F,F,T,F,F,T,T)) /\
  (GF256_by_9 (F,T,F,F,T,T,T,F) = (F,F,F,F,T,F,F,F)) /\
  (GF256_by_9 (F,T,F,F,T,T,T,T) = (F,F,F,F,F,F,F,T)) /\
  (GF256_by_9 (F,T,F,T,F,F,F,F) = (T,T,T,F,F,T,T,F)) /\
  (GF256_by_9 (F,T,F,T,F,F,F,T) = (T,T,T,F,T,T,T,T)) /\
  (GF256_by_9 (F,T,F,T,F,F,T,F) = (T,T,T,T,F,T,F,F)) /\
  (GF256_by_9 (F,T,F,T,F,F,T,T) = (T,T,T,T,T,T,F,T)) /\
  (GF256_by_9 (F,T,F,T,F,T,F,F) = (T,T,F,F,F,F,T,F)) /\
  (GF256_by_9 (F,T,F,T,F,T,F,T) = (T,T,F,F,T,F,T,T)) /\
  (GF256_by_9 (F,T,F,T,F,T,T,F) = (T,T,F,T,F,F,F,F)) /\
  (GF256_by_9 (F,T,F,T,F,T,T,T) = (T,T,F,T,T,F,F,T)) /\
  (GF256_by_9 (F,T,F,T,T,F,F,F) = (T,F,T,F,T,T,T,F)) /\
  (GF256_by_9 (F,T,F,T,T,F,F,T) = (T,F,T,F,F,T,T,T)) /\
  (GF256_by_9 (F,T,F,T,T,F,T,F) = (T,F,T,T,T,T,F,F)) /\
  (GF256_by_9 (F,T,F,T,T,F,T,T) = (T,F,T,T,F,T,F,T)) /\
  (GF256_by_9 (F,T,F,T,T,T,F,F) = (T,F,F,F,T,F,T,F)) /\
  (GF256_by_9 (F,T,F,T,T,T,F,T) = (T,F,F,F,F,F,T,T)) /\
  (GF256_by_9 (F,T,F,T,T,T,T,F) = (T,F,F,T,T,F,F,F)) /\
  (GF256_by_9 (F,T,F,T,T,T,T,T) = (T,F,F,T,F,F,F,T)) /\
  (GF256_by_9 (F,T,T,F,F,F,F,F) = (F,T,F,F,T,T,F,T)) /\
  (GF256_by_9 (F,T,T,F,F,F,F,T) = (F,T,F,F,F,T,F,F)) /\
  (GF256_by_9 (F,T,T,F,F,F,T,F) = (F,T,F,T,T,T,T,T)) /\
  (GF256_by_9 (F,T,T,F,F,F,T,T) = (F,T,F,T,F,T,T,F)) /\
  (GF256_by_9 (F,T,T,F,F,T,F,F) = (F,T,T,F,T,F,F,T)) /\
  (GF256_by_9 (F,T,T,F,F,T,F,T) = (F,T,T,F,F,F,F,F)) /\
  (GF256_by_9 (F,T,T,F,F,T,T,F) = (F,T,T,T,T,F,T,T)) /\
  (GF256_by_9 (F,T,T,F,F,T,T,T) = (F,T,T,T,F,F,T,F)) /\
  (GF256_by_9 (F,T,T,F,T,F,F,F) = (F,F,F,F,F,T,F,T)) /\
  (GF256_by_9 (F,T,T,F,T,F,F,T) = (F,F,F,F,T,T,F,F)) /\
  (GF256_by_9 (F,T,T,F,T,F,T,F) = (F,F,F,T,F,T,T,T)) /\
  (GF256_by_9 (F,T,T,F,T,F,T,T) = (F,F,F,T,T,T,T,F)) /\
  (GF256_by_9 (F,T,T,F,T,T,F,F) = (F,F,T,F,F,F,F,T)) /\
  (GF256_by_9 (F,T,T,F,T,T,F,T) = (F,F,T,F,T,F,F,F)) /\
  (GF256_by_9 (F,T,T,F,T,T,T,F) = (F,F,T,T,F,F,T,T)) /\
  (GF256_by_9 (F,T,T,F,T,T,T,T) = (F,F,T,T,T,F,T,F)) /\
  (GF256_by_9 (F,T,T,T,F,F,F,F) = (T,T,F,T,T,T,F,T)) /\
  (GF256_by_9 (F,T,T,T,F,F,F,T) = (T,T,F,T,F,T,F,F)) /\
  (GF256_by_9 (F,T,T,T,F,F,T,F) = (T,T,F,F,T,T,T,T)) /\
  (GF256_by_9 (F,T,T,T,F,F,T,T) = (T,T,F,F,F,T,T,F)) /\
  (GF256_by_9 (F,T,T,T,F,T,F,F) = (T,T,T,T,T,F,F,T)) /\
  (GF256_by_9 (F,T,T,T,F,T,F,T) = (T,T,T,T,F,F,F,F)) /\
  (GF256_by_9 (F,T,T,T,F,T,T,F) = (T,T,T,F,T,F,T,T)) /\
  (GF256_by_9 (F,T,T,T,F,T,T,T) = (T,T,T,F,F,F,T,F)) /\
  (GF256_by_9 (F,T,T,T,T,F,F,F) = (T,F,F,T,F,T,F,T)) /\
  (GF256_by_9 (F,T,T,T,T,F,F,T) = (T,F,F,T,T,T,F,F)) /\
  (GF256_by_9 (F,T,T,T,T,F,T,F) = (T,F,F,F,F,T,T,T)) /\
  (GF256_by_9 (F,T,T,T,T,F,T,T) = (T,F,F,F,T,T,T,F)) /\
  (GF256_by_9 (F,T,T,T,T,T,F,F) = (T,F,T,T,F,F,F,T)) /\
  (GF256_by_9 (F,T,T,T,T,T,F,T) = (T,F,T,T,T,F,F,F)) /\
  (GF256_by_9 (F,T,T,T,T,T,T,F) = (T,F,T,F,F,F,T,T)) /\
  (GF256_by_9 (F,T,T,T,T,T,T,T) = (T,F,T,F,T,F,T,F)) /\
  (GF256_by_9 (T,F,F,F,F,F,F,F) = (T,T,T,F,T,T,F,F)) /\
  (GF256_by_9 (T,F,F,F,F,F,F,T) = (T,T,T,F,F,T,F,T)) /\
  (GF256_by_9 (T,F,F,F,F,F,T,F) = (T,T,T,T,T,T,T,F)) /\
  (GF256_by_9 (T,F,F,F,F,F,T,T) = (T,T,T,T,F,T,T,T)) /\
  (GF256_by_9 (T,F,F,F,F,T,F,F) = (T,T,F,F,T,F,F,F)) /\
  (GF256_by_9 (T,F,F,F,F,T,F,T) = (T,T,F,F,F,F,F,T)) /\
  (GF256_by_9 (T,F,F,F,F,T,T,F) = (T,T,F,T,T,F,T,F)) /\
  (GF256_by_9 (T,F,F,F,F,T,T,T) = (T,T,F,T,F,F,T,T)) /\
  (GF256_by_9 (T,F,F,F,T,F,F,F) = (T,F,T,F,F,T,F,F)) /\
  (GF256_by_9 (T,F,F,F,T,F,F,T) = (T,F,T,F,T,T,F,T)) /\
  (GF256_by_9 (T,F,F,F,T,F,T,F) = (T,F,T,T,F,T,T,F)) /\
  (GF256_by_9 (T,F,F,F,T,F,T,T) = (T,F,T,T,T,T,T,T)) /\
  (GF256_by_9 (T,F,F,F,T,T,F,F) = (T,F,F,F,F,F,F,F)) /\
  (GF256_by_9 (T,F,F,F,T,T,F,T) = (T,F,F,F,T,F,F,T)) /\
  (GF256_by_9 (T,F,F,F,T,T,T,F) = (T,F,F,T,F,F,T,F)) /\
  (GF256_by_9 (T,F,F,F,T,T,T,T) = (T,F,F,T,T,F,T,T)) /\
  (GF256_by_9 (T,F,F,T,F,F,F,F) = (F,T,T,T,T,T,F,F)) /\
  (GF256_by_9 (T,F,F,T,F,F,F,T) = (F,T,T,T,F,T,F,T)) /\
  (GF256_by_9 (T,F,F,T,F,F,T,F) = (F,T,T,F,T,T,T,F)) /\
  (GF256_by_9 (T,F,F,T,F,F,T,T) = (F,T,T,F,F,T,T,T)) /\
  (GF256_by_9 (T,F,F,T,F,T,F,F) = (F,T,F,T,T,F,F,F)) /\
  (GF256_by_9 (T,F,F,T,F,T,F,T) = (F,T,F,T,F,F,F,T)) /\
  (GF256_by_9 (T,F,F,T,F,T,T,F) = (F,T,F,F,T,F,T,F)) /\
  (GF256_by_9 (T,F,F,T,F,T,T,T) = (F,T,F,F,F,F,T,T)) /\
  (GF256_by_9 (T,F,F,T,T,F,F,F) = (F,F,T,T,F,T,F,F)) /\
  (GF256_by_9 (T,F,F,T,T,F,F,T) = (F,F,T,T,T,T,F,T)) /\
  (GF256_by_9 (T,F,F,T,T,F,T,F) = (F,F,T,F,F,T,T,F)) /\
  (GF256_by_9 (T,F,F,T,T,F,T,T) = (F,F,T,F,T,T,T,T)) /\
  (GF256_by_9 (T,F,F,T,T,T,F,F) = (F,F,F,T,F,F,F,F)) /\
  (GF256_by_9 (T,F,F,T,T,T,F,T) = (F,F,F,T,T,F,F,T)) /\
  (GF256_by_9 (T,F,F,T,T,T,T,F) = (F,F,F,F,F,F,T,F)) /\
  (GF256_by_9 (T,F,F,T,T,T,T,T) = (F,F,F,F,T,F,T,T)) /\
  (GF256_by_9 (T,F,T,F,F,F,F,F) = (T,T,F,T,F,T,T,T)) /\
  (GF256_by_9 (T,F,T,F,F,F,F,T) = (T,T,F,T,T,T,T,F)) /\
  (GF256_by_9 (T,F,T,F,F,F,T,F) = (T,T,F,F,F,T,F,T)) /\
  (GF256_by_9 (T,F,T,F,F,F,T,T) = (T,T,F,F,T,T,F,F)) /\
  (GF256_by_9 (T,F,T,F,F,T,F,F) = (T,T,T,T,F,F,T,T)) /\
  (GF256_by_9 (T,F,T,F,F,T,F,T) = (T,T,T,T,T,F,T,F)) /\
  (GF256_by_9 (T,F,T,F,F,T,T,F) = (T,T,T,F,F,F,F,T)) /\
  (GF256_by_9 (T,F,T,F,F,T,T,T) = (T,T,T,F,T,F,F,F)) /\
  (GF256_by_9 (T,F,T,F,T,F,F,F) = (T,F,F,T,T,T,T,T)) /\
  (GF256_by_9 (T,F,T,F,T,F,F,T) = (T,F,F,T,F,T,T,F)) /\
  (GF256_by_9 (T,F,T,F,T,F,T,F) = (T,F,F,F,T,T,F,T)) /\
  (GF256_by_9 (T,F,T,F,T,F,T,T) = (T,F,F,F,F,T,F,F)) /\
  (GF256_by_9 (T,F,T,F,T,T,F,F) = (T,F,T,T,T,F,T,T)) /\
  (GF256_by_9 (T,F,T,F,T,T,F,T) = (T,F,T,T,F,F,T,F)) /\
  (GF256_by_9 (T,F,T,F,T,T,T,F) = (T,F,T,F,T,F,F,T)) /\
  (GF256_by_9 (T,F,T,F,T,T,T,T) = (T,F,T,F,F,F,F,F)) /\
  (GF256_by_9 (T,F,T,T,F,F,F,F) = (F,T,F,F,F,T,T,T)) /\
  (GF256_by_9 (T,F,T,T,F,F,F,T) = (F,T,F,F,T,T,T,F)) /\
  (GF256_by_9 (T,F,T,T,F,F,T,F) = (F,T,F,T,F,T,F,T)) /\
  (GF256_by_9 (T,F,T,T,F,F,T,T) = (F,T,F,T,T,T,F,F)) /\
  (GF256_by_9 (T,F,T,T,F,T,F,F) = (F,T,T,F,F,F,T,T)) /\
  (GF256_by_9 (T,F,T,T,F,T,F,T) = (F,T,T,F,T,F,T,F)) /\
  (GF256_by_9 (T,F,T,T,F,T,T,F) = (F,T,T,T,F,F,F,T)) /\
  (GF256_by_9 (T,F,T,T,F,T,T,T) = (F,T,T,T,T,F,F,F)) /\
  (GF256_by_9 (T,F,T,T,T,F,F,F) = (F,F,F,F,T,T,T,T)) /\
  (GF256_by_9 (T,F,T,T,T,F,F,T) = (F,F,F,F,F,T,T,F)) /\
  (GF256_by_9 (T,F,T,T,T,F,T,F) = (F,F,F,T,T,T,F,T)) /\
  (GF256_by_9 (T,F,T,T,T,F,T,T) = (F,F,F,T,F,T,F,F)) /\
  (GF256_by_9 (T,F,T,T,T,T,F,F) = (F,F,T,F,T,F,T,T)) /\
  (GF256_by_9 (T,F,T,T,T,T,F,T) = (F,F,T,F,F,F,T,F)) /\
  (GF256_by_9 (T,F,T,T,T,T,T,F) = (F,F,T,T,T,F,F,T)) /\
  (GF256_by_9 (T,F,T,T,T,T,T,T) = (F,F,T,T,F,F,F,F)) /\
  (GF256_by_9 (T,T,F,F,F,F,F,F) = (T,F,F,T,T,F,T,F)) /\
  (GF256_by_9 (T,T,F,F,F,F,F,T) = (T,F,F,T,F,F,T,T)) /\
  (GF256_by_9 (T,T,F,F,F,F,T,F) = (T,F,F,F,T,F,F,F)) /\
  (GF256_by_9 (T,T,F,F,F,F,T,T) = (T,F,F,F,F,F,F,T)) /\
  (GF256_by_9 (T,T,F,F,F,T,F,F) = (T,F,T,T,T,T,T,F)) /\
  (GF256_by_9 (T,T,F,F,F,T,F,T) = (T,F,T,T,F,T,T,T)) /\
  (GF256_by_9 (T,T,F,F,F,T,T,F) = (T,F,T,F,T,T,F,F)) /\
  (GF256_by_9 (T,T,F,F,F,T,T,T) = (T,F,T,F,F,T,F,T)) /\
  (GF256_by_9 (T,T,F,F,T,F,F,F) = (T,T,F,T,F,F,T,F)) /\
  (GF256_by_9 (T,T,F,F,T,F,F,T) = (T,T,F,T,T,F,T,T)) /\
  (GF256_by_9 (T,T,F,F,T,F,T,F) = (T,T,F,F,F,F,F,F)) /\
  (GF256_by_9 (T,T,F,F,T,F,T,T) = (T,T,F,F,T,F,F,T)) /\
  (GF256_by_9 (T,T,F,F,T,T,F,F) = (T,T,T,T,F,T,T,F)) /\
  (GF256_by_9 (T,T,F,F,T,T,F,T) = (T,T,T,T,T,T,T,T)) /\
  (GF256_by_9 (T,T,F,F,T,T,T,F) = (T,T,T,F,F,T,F,F)) /\
  (GF256_by_9 (T,T,F,F,T,T,T,T) = (T,T,T,F,T,T,F,T)) /\
  (GF256_by_9 (T,T,F,T,F,F,F,F) = (F,F,F,F,T,F,T,F)) /\
  (GF256_by_9 (T,T,F,T,F,F,F,T) = (F,F,F,F,F,F,T,T)) /\
  (GF256_by_9 (T,T,F,T,F,F,T,F) = (F,F,F,T,T,F,F,F)) /\
  (GF256_by_9 (T,T,F,T,F,F,T,T) = (F,F,F,T,F,F,F,T)) /\
  (GF256_by_9 (T,T,F,T,F,T,F,F) = (F,F,T,F,T,T,T,F)) /\
  (GF256_by_9 (T,T,F,T,F,T,F,T) = (F,F,T,F,F,T,T,T)) /\
  (GF256_by_9 (T,T,F,T,F,T,T,F) = (F,F,T,T,T,T,F,F)) /\
  (GF256_by_9 (T,T,F,T,F,T,T,T) = (F,F,T,T,F,T,F,T)) /\
  (GF256_by_9 (T,T,F,T,T,F,F,F) = (F,T,F,F,F,F,T,F)) /\
  (GF256_by_9 (T,T,F,T,T,F,F,T) = (F,T,F,F,T,F,T,T)) /\
  (GF256_by_9 (T,T,F,T,T,F,T,F) = (F,T,F,T,F,F,F,F)) /\
  (GF256_by_9 (T,T,F,T,T,F,T,T) = (F,T,F,T,T,F,F,T)) /\
  (GF256_by_9 (T,T,F,T,T,T,F,F) = (F,T,T,F,F,T,T,F)) /\
  (GF256_by_9 (T,T,F,T,T,T,F,T) = (F,T,T,F,T,T,T,T)) /\
  (GF256_by_9 (T,T,F,T,T,T,T,F) = (F,T,T,T,F,T,F,F)) /\
  (GF256_by_9 (T,T,F,T,T,T,T,T) = (F,T,T,T,T,T,F,T)) /\
  (GF256_by_9 (T,T,T,F,F,F,F,F) = (T,F,T,F,F,F,F,T)) /\
  (GF256_by_9 (T,T,T,F,F,F,F,T) = (T,F,T,F,T,F,F,F)) /\
  (GF256_by_9 (T,T,T,F,F,F,T,F) = (T,F,T,T,F,F,T,T)) /\
  (GF256_by_9 (T,T,T,F,F,F,T,T) = (T,F,T,T,T,F,T,F)) /\
  (GF256_by_9 (T,T,T,F,F,T,F,F) = (T,F,F,F,F,T,F,T)) /\
  (GF256_by_9 (T,T,T,F,F,T,F,T) = (T,F,F,F,T,T,F,F)) /\
  (GF256_by_9 (T,T,T,F,F,T,T,F) = (T,F,F,T,F,T,T,T)) /\
  (GF256_by_9 (T,T,T,F,F,T,T,T) = (T,F,F,T,T,T,T,F)) /\
  (GF256_by_9 (T,T,T,F,T,F,F,F) = (T,T,T,F,T,F,F,T)) /\
  (GF256_by_9 (T,T,T,F,T,F,F,T) = (T,T,T,F,F,F,F,F)) /\
  (GF256_by_9 (T,T,T,F,T,F,T,F) = (T,T,T,T,T,F,T,T)) /\
  (GF256_by_9 (T,T,T,F,T,F,T,T) = (T,T,T,T,F,F,T,F)) /\
  (GF256_by_9 (T,T,T,F,T,T,F,F) = (T,T,F,F,T,T,F,T)) /\
  (GF256_by_9 (T,T,T,F,T,T,F,T) = (T,T,F,F,F,T,F,F)) /\
  (GF256_by_9 (T,T,T,F,T,T,T,F) = (T,T,F,T,T,T,T,T)) /\
  (GF256_by_9 (T,T,T,F,T,T,T,T) = (T,T,F,T,F,T,T,F)) /\
  (GF256_by_9 (T,T,T,T,F,F,F,F) = (F,F,T,T,F,F,F,T)) /\
  (GF256_by_9 (T,T,T,T,F,F,F,T) = (F,F,T,T,T,F,F,F)) /\
  (GF256_by_9 (T,T,T,T,F,F,T,F) = (F,F,T,F,F,F,T,T)) /\
  (GF256_by_9 (T,T,T,T,F,F,T,T) = (F,F,T,F,T,F,T,F)) /\
  (GF256_by_9 (T,T,T,T,F,T,F,F) = (F,F,F,T,F,T,F,T)) /\
  (GF256_by_9 (T,T,T,T,F,T,F,T) = (F,F,F,T,T,T,F,F)) /\
  (GF256_by_9 (T,T,T,T,F,T,T,F) = (F,F,F,F,F,T,T,T)) /\
  (GF256_by_9 (T,T,T,T,F,T,T,T) = (F,F,F,F,T,T,T,F)) /\
  (GF256_by_9 (T,T,T,T,T,F,F,F) = (F,T,T,T,T,F,F,T)) /\
  (GF256_by_9 (T,T,T,T,T,F,F,T) = (F,T,T,T,F,F,F,F)) /\
  (GF256_by_9 (T,T,T,T,T,F,T,F) = (F,T,T,F,T,F,T,T)) /\
  (GF256_by_9 (T,T,T,T,T,F,T,T) = (F,T,T,F,F,F,T,F)) /\
  (GF256_by_9 (T,T,T,T,T,T,F,F) = (F,T,F,T,T,T,F,T)) /\
  (GF256_by_9 (T,T,T,T,T,T,F,T) = (F,T,F,T,F,T,F,F)) /\
  (GF256_by_9 (T,T,T,T,T,T,T,F) = (F,T,F,F,T,T,T,T)) /\
  (GF256_by_9 (T,T,T,T,T,T,T,T) = (F,T,F,F,F,T,T,F))`;

val GF256_by_11_def = Count.apply Define
 `(GF256_by_11 (F,F,F,F,F,F,F,F) = (F,F,F,F,F,F,F,F)) /\
  (GF256_by_11 (F,F,F,F,F,F,F,T) = (F,F,F,F,T,F,T,T)) /\
  (GF256_by_11 (F,F,F,F,F,F,T,F) = (F,F,F,T,F,T,T,F)) /\
  (GF256_by_11 (F,F,F,F,F,F,T,T) = (F,F,F,T,T,T,F,T)) /\
  (GF256_by_11 (F,F,F,F,F,T,F,F) = (F,F,T,F,T,T,F,F)) /\
  (GF256_by_11 (F,F,F,F,F,T,F,T) = (F,F,T,F,F,T,T,T)) /\
  (GF256_by_11 (F,F,F,F,F,T,T,F) = (F,F,T,T,T,F,T,F)) /\
  (GF256_by_11 (F,F,F,F,F,T,T,T) = (F,F,T,T,F,F,F,T)) /\
  (GF256_by_11 (F,F,F,F,T,F,F,F) = (F,T,F,T,T,F,F,F)) /\
  (GF256_by_11 (F,F,F,F,T,F,F,T) = (F,T,F,T,F,F,T,T)) /\
  (GF256_by_11 (F,F,F,F,T,F,T,F) = (F,T,F,F,T,T,T,F)) /\
  (GF256_by_11 (F,F,F,F,T,F,T,T) = (F,T,F,F,F,T,F,T)) /\
  (GF256_by_11 (F,F,F,F,T,T,F,F) = (F,T,T,T,F,T,F,F)) /\
  (GF256_by_11 (F,F,F,F,T,T,F,T) = (F,T,T,T,T,T,T,T)) /\
  (GF256_by_11 (F,F,F,F,T,T,T,F) = (F,T,T,F,F,F,T,F)) /\
  (GF256_by_11 (F,F,F,F,T,T,T,T) = (F,T,T,F,T,F,F,T)) /\
  (GF256_by_11 (F,F,F,T,F,F,F,F) = (T,F,T,T,F,F,F,F)) /\
  (GF256_by_11 (F,F,F,T,F,F,F,T) = (T,F,T,T,T,F,T,T)) /\
  (GF256_by_11 (F,F,F,T,F,F,T,F) = (T,F,T,F,F,T,T,F)) /\
  (GF256_by_11 (F,F,F,T,F,F,T,T) = (T,F,T,F,T,T,F,T)) /\
  (GF256_by_11 (F,F,F,T,F,T,F,F) = (T,F,F,T,T,T,F,F)) /\
  (GF256_by_11 (F,F,F,T,F,T,F,T) = (T,F,F,T,F,T,T,T)) /\
  (GF256_by_11 (F,F,F,T,F,T,T,F) = (T,F,F,F,T,F,T,F)) /\
  (GF256_by_11 (F,F,F,T,F,T,T,T) = (T,F,F,F,F,F,F,T)) /\
  (GF256_by_11 (F,F,F,T,T,F,F,F) = (T,T,T,F,T,F,F,F)) /\
  (GF256_by_11 (F,F,F,T,T,F,F,T) = (T,T,T,F,F,F,T,T)) /\
  (GF256_by_11 (F,F,F,T,T,F,T,F) = (T,T,T,T,T,T,T,F)) /\
  (GF256_by_11 (F,F,F,T,T,F,T,T) = (T,T,T,T,F,T,F,T)) /\
  (GF256_by_11 (F,F,F,T,T,T,F,F) = (T,T,F,F,F,T,F,F)) /\
  (GF256_by_11 (F,F,F,T,T,T,F,T) = (T,T,F,F,T,T,T,T)) /\
  (GF256_by_11 (F,F,F,T,T,T,T,F) = (T,T,F,T,F,F,T,F)) /\
  (GF256_by_11 (F,F,F,T,T,T,T,T) = (T,T,F,T,T,F,F,T)) /\
  (GF256_by_11 (F,F,T,F,F,F,F,F) = (F,T,T,T,T,F,T,T)) /\
  (GF256_by_11 (F,F,T,F,F,F,F,T) = (F,T,T,T,F,F,F,F)) /\
  (GF256_by_11 (F,F,T,F,F,F,T,F) = (F,T,T,F,T,T,F,T)) /\
  (GF256_by_11 (F,F,T,F,F,F,T,T) = (F,T,T,F,F,T,T,F)) /\
  (GF256_by_11 (F,F,T,F,F,T,F,F) = (F,T,F,T,F,T,T,T)) /\
  (GF256_by_11 (F,F,T,F,F,T,F,T) = (F,T,F,T,T,T,F,F)) /\
  (GF256_by_11 (F,F,T,F,F,T,T,F) = (F,T,F,F,F,F,F,T)) /\
  (GF256_by_11 (F,F,T,F,F,T,T,T) = (F,T,F,F,T,F,T,F)) /\
  (GF256_by_11 (F,F,T,F,T,F,F,F) = (F,F,T,F,F,F,T,T)) /\
  (GF256_by_11 (F,F,T,F,T,F,F,T) = (F,F,T,F,T,F,F,F)) /\
  (GF256_by_11 (F,F,T,F,T,F,T,F) = (F,F,T,T,F,T,F,T)) /\
  (GF256_by_11 (F,F,T,F,T,F,T,T) = (F,F,T,T,T,T,T,F)) /\
  (GF256_by_11 (F,F,T,F,T,T,F,F) = (F,F,F,F,T,T,T,T)) /\
  (GF256_by_11 (F,F,T,F,T,T,F,T) = (F,F,F,F,F,T,F,F)) /\
  (GF256_by_11 (F,F,T,F,T,T,T,F) = (F,F,F,T,T,F,F,T)) /\
  (GF256_by_11 (F,F,T,F,T,T,T,T) = (F,F,F,T,F,F,T,F)) /\
  (GF256_by_11 (F,F,T,T,F,F,F,F) = (T,T,F,F,T,F,T,T)) /\
  (GF256_by_11 (F,F,T,T,F,F,F,T) = (T,T,F,F,F,F,F,F)) /\
  (GF256_by_11 (F,F,T,T,F,F,T,F) = (T,T,F,T,T,T,F,T)) /\
  (GF256_by_11 (F,F,T,T,F,F,T,T) = (T,T,F,T,F,T,T,F)) /\
  (GF256_by_11 (F,F,T,T,F,T,F,F) = (T,T,T,F,F,T,T,T)) /\
  (GF256_by_11 (F,F,T,T,F,T,F,T) = (T,T,T,F,T,T,F,F)) /\
  (GF256_by_11 (F,F,T,T,F,T,T,F) = (T,T,T,T,F,F,F,T)) /\
  (GF256_by_11 (F,F,T,T,F,T,T,T) = (T,T,T,T,T,F,T,F)) /\
  (GF256_by_11 (F,F,T,T,T,F,F,F) = (T,F,F,T,F,F,T,T)) /\
  (GF256_by_11 (F,F,T,T,T,F,F,T) = (T,F,F,T,T,F,F,F)) /\
  (GF256_by_11 (F,F,T,T,T,F,T,F) = (T,F,F,F,F,T,F,T)) /\
  (GF256_by_11 (F,F,T,T,T,F,T,T) = (T,F,F,F,T,T,T,F)) /\
  (GF256_by_11 (F,F,T,T,T,T,F,F) = (T,F,T,T,T,T,T,T)) /\
  (GF256_by_11 (F,F,T,T,T,T,F,T) = (T,F,T,T,F,T,F,F)) /\
  (GF256_by_11 (F,F,T,T,T,T,T,F) = (T,F,T,F,T,F,F,T)) /\
  (GF256_by_11 (F,F,T,T,T,T,T,T) = (T,F,T,F,F,F,T,F)) /\
  (GF256_by_11 (F,T,F,F,F,F,F,F) = (T,T,T,T,F,T,T,F)) /\
  (GF256_by_11 (F,T,F,F,F,F,F,T) = (T,T,T,T,T,T,F,T)) /\
  (GF256_by_11 (F,T,F,F,F,F,T,F) = (T,T,T,F,F,F,F,F)) /\
  (GF256_by_11 (F,T,F,F,F,F,T,T) = (T,T,T,F,T,F,T,T)) /\
  (GF256_by_11 (F,T,F,F,F,T,F,F) = (T,T,F,T,T,F,T,F)) /\
  (GF256_by_11 (F,T,F,F,F,T,F,T) = (T,T,F,T,F,F,F,T)) /\
  (GF256_by_11 (F,T,F,F,F,T,T,F) = (T,T,F,F,T,T,F,F)) /\
  (GF256_by_11 (F,T,F,F,F,T,T,T) = (T,T,F,F,F,T,T,T)) /\
  (GF256_by_11 (F,T,F,F,T,F,F,F) = (T,F,T,F,T,T,T,F)) /\
  (GF256_by_11 (F,T,F,F,T,F,F,T) = (T,F,T,F,F,T,F,T)) /\
  (GF256_by_11 (F,T,F,F,T,F,T,F) = (T,F,T,T,T,F,F,F)) /\
  (GF256_by_11 (F,T,F,F,T,F,T,T) = (T,F,T,T,F,F,T,T)) /\
  (GF256_by_11 (F,T,F,F,T,T,F,F) = (T,F,F,F,F,F,T,F)) /\
  (GF256_by_11 (F,T,F,F,T,T,F,T) = (T,F,F,F,T,F,F,T)) /\
  (GF256_by_11 (F,T,F,F,T,T,T,F) = (T,F,F,T,F,T,F,F)) /\
  (GF256_by_11 (F,T,F,F,T,T,T,T) = (T,F,F,T,T,T,T,T)) /\
  (GF256_by_11 (F,T,F,T,F,F,F,F) = (F,T,F,F,F,T,T,F)) /\
  (GF256_by_11 (F,T,F,T,F,F,F,T) = (F,T,F,F,T,T,F,T)) /\
  (GF256_by_11 (F,T,F,T,F,F,T,F) = (F,T,F,T,F,F,F,F)) /\
  (GF256_by_11 (F,T,F,T,F,F,T,T) = (F,T,F,T,T,F,T,T)) /\
  (GF256_by_11 (F,T,F,T,F,T,F,F) = (F,T,T,F,T,F,T,F)) /\
  (GF256_by_11 (F,T,F,T,F,T,F,T) = (F,T,T,F,F,F,F,T)) /\
  (GF256_by_11 (F,T,F,T,F,T,T,F) = (F,T,T,T,T,T,F,F)) /\
  (GF256_by_11 (F,T,F,T,F,T,T,T) = (F,T,T,T,F,T,T,T)) /\
  (GF256_by_11 (F,T,F,T,T,F,F,F) = (F,F,F,T,T,T,T,F)) /\
  (GF256_by_11 (F,T,F,T,T,F,F,T) = (F,F,F,T,F,T,F,T)) /\
  (GF256_by_11 (F,T,F,T,T,F,T,F) = (F,F,F,F,T,F,F,F)) /\
  (GF256_by_11 (F,T,F,T,T,F,T,T) = (F,F,F,F,F,F,T,T)) /\
  (GF256_by_11 (F,T,F,T,T,T,F,F) = (F,F,T,T,F,F,T,F)) /\
  (GF256_by_11 (F,T,F,T,T,T,F,T) = (F,F,T,T,T,F,F,T)) /\
  (GF256_by_11 (F,T,F,T,T,T,T,F) = (F,F,T,F,F,T,F,F)) /\
  (GF256_by_11 (F,T,F,T,T,T,T,T) = (F,F,T,F,T,T,T,T)) /\
  (GF256_by_11 (F,T,T,F,F,F,F,F) = (T,F,F,F,T,T,F,T)) /\
  (GF256_by_11 (F,T,T,F,F,F,F,T) = (T,F,F,F,F,T,T,F)) /\
  (GF256_by_11 (F,T,T,F,F,F,T,F) = (T,F,F,T,T,F,T,T)) /\
  (GF256_by_11 (F,T,T,F,F,F,T,T) = (T,F,F,T,F,F,F,F)) /\
  (GF256_by_11 (F,T,T,F,F,T,F,F) = (T,F,T,F,F,F,F,T)) /\
  (GF256_by_11 (F,T,T,F,F,T,F,T) = (T,F,T,F,T,F,T,F)) /\
  (GF256_by_11 (F,T,T,F,F,T,T,F) = (T,F,T,T,F,T,T,T)) /\
  (GF256_by_11 (F,T,T,F,F,T,T,T) = (T,F,T,T,T,T,F,F)) /\
  (GF256_by_11 (F,T,T,F,T,F,F,F) = (T,T,F,T,F,T,F,T)) /\
  (GF256_by_11 (F,T,T,F,T,F,F,T) = (T,T,F,T,T,T,T,F)) /\
  (GF256_by_11 (F,T,T,F,T,F,T,F) = (T,T,F,F,F,F,T,T)) /\
  (GF256_by_11 (F,T,T,F,T,F,T,T) = (T,T,F,F,T,F,F,F)) /\
  (GF256_by_11 (F,T,T,F,T,T,F,F) = (T,T,T,T,T,F,F,T)) /\
  (GF256_by_11 (F,T,T,F,T,T,F,T) = (T,T,T,T,F,F,T,F)) /\
  (GF256_by_11 (F,T,T,F,T,T,T,F) = (T,T,T,F,T,T,T,T)) /\
  (GF256_by_11 (F,T,T,F,T,T,T,T) = (T,T,T,F,F,T,F,F)) /\
  (GF256_by_11 (F,T,T,T,F,F,F,F) = (F,F,T,T,T,T,F,T)) /\
  (GF256_by_11 (F,T,T,T,F,F,F,T) = (F,F,T,T,F,T,T,F)) /\
  (GF256_by_11 (F,T,T,T,F,F,T,F) = (F,F,T,F,T,F,T,T)) /\
  (GF256_by_11 (F,T,T,T,F,F,T,T) = (F,F,T,F,F,F,F,F)) /\
  (GF256_by_11 (F,T,T,T,F,T,F,F) = (F,F,F,T,F,F,F,T)) /\
  (GF256_by_11 (F,T,T,T,F,T,F,T) = (F,F,F,T,T,F,T,F)) /\
  (GF256_by_11 (F,T,T,T,F,T,T,F) = (F,F,F,F,F,T,T,T)) /\
  (GF256_by_11 (F,T,T,T,F,T,T,T) = (F,F,F,F,T,T,F,F)) /\
  (GF256_by_11 (F,T,T,T,T,F,F,F) = (F,T,T,F,F,T,F,T)) /\
  (GF256_by_11 (F,T,T,T,T,F,F,T) = (F,T,T,F,T,T,T,F)) /\
  (GF256_by_11 (F,T,T,T,T,F,T,F) = (F,T,T,T,F,F,T,T)) /\
  (GF256_by_11 (F,T,T,T,T,F,T,T) = (F,T,T,T,T,F,F,F)) /\
  (GF256_by_11 (F,T,T,T,T,T,F,F) = (F,T,F,F,T,F,F,T)) /\
  (GF256_by_11 (F,T,T,T,T,T,F,T) = (F,T,F,F,F,F,T,F)) /\
  (GF256_by_11 (F,T,T,T,T,T,T,F) = (F,T,F,T,T,T,T,T)) /\
  (GF256_by_11 (F,T,T,T,T,T,T,T) = (F,T,F,T,F,T,F,F)) /\
  (GF256_by_11 (T,F,F,F,F,F,F,F) = (T,T,T,T,F,T,T,T)) /\
  (GF256_by_11 (T,F,F,F,F,F,F,T) = (T,T,T,T,T,T,F,F)) /\
  (GF256_by_11 (T,F,F,F,F,F,T,F) = (T,T,T,F,F,F,F,T)) /\
  (GF256_by_11 (T,F,F,F,F,F,T,T) = (T,T,T,F,T,F,T,F)) /\
  (GF256_by_11 (T,F,F,F,F,T,F,F) = (T,T,F,T,T,F,T,T)) /\
  (GF256_by_11 (T,F,F,F,F,T,F,T) = (T,T,F,T,F,F,F,F)) /\
  (GF256_by_11 (T,F,F,F,F,T,T,F) = (T,T,F,F,T,T,F,T)) /\
  (GF256_by_11 (T,F,F,F,F,T,T,T) = (T,T,F,F,F,T,T,F)) /\
  (GF256_by_11 (T,F,F,F,T,F,F,F) = (T,F,T,F,T,T,T,T)) /\
  (GF256_by_11 (T,F,F,F,T,F,F,T) = (T,F,T,F,F,T,F,F)) /\
  (GF256_by_11 (T,F,F,F,T,F,T,F) = (T,F,T,T,T,F,F,T)) /\
  (GF256_by_11 (T,F,F,F,T,F,T,T) = (T,F,T,T,F,F,T,F)) /\
  (GF256_by_11 (T,F,F,F,T,T,F,F) = (T,F,F,F,F,F,T,T)) /\
  (GF256_by_11 (T,F,F,F,T,T,F,T) = (T,F,F,F,T,F,F,F)) /\
  (GF256_by_11 (T,F,F,F,T,T,T,F) = (T,F,F,T,F,T,F,T)) /\
  (GF256_by_11 (T,F,F,F,T,T,T,T) = (T,F,F,T,T,T,T,F)) /\
  (GF256_by_11 (T,F,F,T,F,F,F,F) = (F,T,F,F,F,T,T,T)) /\
  (GF256_by_11 (T,F,F,T,F,F,F,T) = (F,T,F,F,T,T,F,F)) /\
  (GF256_by_11 (T,F,F,T,F,F,T,F) = (F,T,F,T,F,F,F,T)) /\
  (GF256_by_11 (T,F,F,T,F,F,T,T) = (F,T,F,T,T,F,T,F)) /\
  (GF256_by_11 (T,F,F,T,F,T,F,F) = (F,T,T,F,T,F,T,T)) /\
  (GF256_by_11 (T,F,F,T,F,T,F,T) = (F,T,T,F,F,F,F,F)) /\
  (GF256_by_11 (T,F,F,T,F,T,T,F) = (F,T,T,T,T,T,F,T)) /\
  (GF256_by_11 (T,F,F,T,F,T,T,T) = (F,T,T,T,F,T,T,F)) /\
  (GF256_by_11 (T,F,F,T,T,F,F,F) = (F,F,F,T,T,T,T,T)) /\
  (GF256_by_11 (T,F,F,T,T,F,F,T) = (F,F,F,T,F,T,F,F)) /\
  (GF256_by_11 (T,F,F,T,T,F,T,F) = (F,F,F,F,T,F,F,T)) /\
  (GF256_by_11 (T,F,F,T,T,F,T,T) = (F,F,F,F,F,F,T,F)) /\
  (GF256_by_11 (T,F,F,T,T,T,F,F) = (F,F,T,T,F,F,T,T)) /\
  (GF256_by_11 (T,F,F,T,T,T,F,T) = (F,F,T,T,T,F,F,F)) /\
  (GF256_by_11 (T,F,F,T,T,T,T,F) = (F,F,T,F,F,T,F,T)) /\
  (GF256_by_11 (T,F,F,T,T,T,T,T) = (F,F,T,F,T,T,T,F)) /\
  (GF256_by_11 (T,F,T,F,F,F,F,F) = (T,F,F,F,T,T,F,F)) /\
  (GF256_by_11 (T,F,T,F,F,F,F,T) = (T,F,F,F,F,T,T,T)) /\
  (GF256_by_11 (T,F,T,F,F,F,T,F) = (T,F,F,T,T,F,T,F)) /\
  (GF256_by_11 (T,F,T,F,F,F,T,T) = (T,F,F,T,F,F,F,T)) /\
  (GF256_by_11 (T,F,T,F,F,T,F,F) = (T,F,T,F,F,F,F,F)) /\
  (GF256_by_11 (T,F,T,F,F,T,F,T) = (T,F,T,F,T,F,T,T)) /\
  (GF256_by_11 (T,F,T,F,F,T,T,F) = (T,F,T,T,F,T,T,F)) /\
  (GF256_by_11 (T,F,T,F,F,T,T,T) = (T,F,T,T,T,T,F,T)) /\
  (GF256_by_11 (T,F,T,F,T,F,F,F) = (T,T,F,T,F,T,F,F)) /\
  (GF256_by_11 (T,F,T,F,T,F,F,T) = (T,T,F,T,T,T,T,T)) /\
  (GF256_by_11 (T,F,T,F,T,F,T,F) = (T,T,F,F,F,F,T,F)) /\
  (GF256_by_11 (T,F,T,F,T,F,T,T) = (T,T,F,F,T,F,F,T)) /\
  (GF256_by_11 (T,F,T,F,T,T,F,F) = (T,T,T,T,T,F,F,F)) /\
  (GF256_by_11 (T,F,T,F,T,T,F,T) = (T,T,T,T,F,F,T,T)) /\
  (GF256_by_11 (T,F,T,F,T,T,T,F) = (T,T,T,F,T,T,T,F)) /\
  (GF256_by_11 (T,F,T,F,T,T,T,T) = (T,T,T,F,F,T,F,T)) /\
  (GF256_by_11 (T,F,T,T,F,F,F,F) = (F,F,T,T,T,T,F,F)) /\
  (GF256_by_11 (T,F,T,T,F,F,F,T) = (F,F,T,T,F,T,T,T)) /\
  (GF256_by_11 (T,F,T,T,F,F,T,F) = (F,F,T,F,T,F,T,F)) /\
  (GF256_by_11 (T,F,T,T,F,F,T,T) = (F,F,T,F,F,F,F,T)) /\
  (GF256_by_11 (T,F,T,T,F,T,F,F) = (F,F,F,T,F,F,F,F)) /\
  (GF256_by_11 (T,F,T,T,F,T,F,T) = (F,F,F,T,T,F,T,T)) /\
  (GF256_by_11 (T,F,T,T,F,T,T,F) = (F,F,F,F,F,T,T,F)) /\
  (GF256_by_11 (T,F,T,T,F,T,T,T) = (F,F,F,F,T,T,F,T)) /\
  (GF256_by_11 (T,F,T,T,T,F,F,F) = (F,T,T,F,F,T,F,F)) /\
  (GF256_by_11 (T,F,T,T,T,F,F,T) = (F,T,T,F,T,T,T,T)) /\
  (GF256_by_11 (T,F,T,T,T,F,T,F) = (F,T,T,T,F,F,T,F)) /\
  (GF256_by_11 (T,F,T,T,T,F,T,T) = (F,T,T,T,T,F,F,T)) /\
  (GF256_by_11 (T,F,T,T,T,T,F,F) = (F,T,F,F,T,F,F,F)) /\
  (GF256_by_11 (T,F,T,T,T,T,F,T) = (F,T,F,F,F,F,T,T)) /\
  (GF256_by_11 (T,F,T,T,T,T,T,F) = (F,T,F,T,T,T,T,F)) /\
  (GF256_by_11 (T,F,T,T,T,T,T,T) = (F,T,F,T,F,T,F,T)) /\
  (GF256_by_11 (T,T,F,F,F,F,F,F) = (F,F,F,F,F,F,F,T)) /\
  (GF256_by_11 (T,T,F,F,F,F,F,T) = (F,F,F,F,T,F,T,F)) /\
  (GF256_by_11 (T,T,F,F,F,F,T,F) = (F,F,F,T,F,T,T,T)) /\
  (GF256_by_11 (T,T,F,F,F,F,T,T) = (F,F,F,T,T,T,F,F)) /\
  (GF256_by_11 (T,T,F,F,F,T,F,F) = (F,F,T,F,T,T,F,T)) /\
  (GF256_by_11 (T,T,F,F,F,T,F,T) = (F,F,T,F,F,T,T,F)) /\
  (GF256_by_11 (T,T,F,F,F,T,T,F) = (F,F,T,T,T,F,T,T)) /\
  (GF256_by_11 (T,T,F,F,F,T,T,T) = (F,F,T,T,F,F,F,F)) /\
  (GF256_by_11 (T,T,F,F,T,F,F,F) = (F,T,F,T,T,F,F,T)) /\
  (GF256_by_11 (T,T,F,F,T,F,F,T) = (F,T,F,T,F,F,T,F)) /\
  (GF256_by_11 (T,T,F,F,T,F,T,F) = (F,T,F,F,T,T,T,T)) /\
  (GF256_by_11 (T,T,F,F,T,F,T,T) = (F,T,F,F,F,T,F,F)) /\
  (GF256_by_11 (T,T,F,F,T,T,F,F) = (F,T,T,T,F,T,F,T)) /\
  (GF256_by_11 (T,T,F,F,T,T,F,T) = (F,T,T,T,T,T,T,F)) /\
  (GF256_by_11 (T,T,F,F,T,T,T,F) = (F,T,T,F,F,F,T,T)) /\
  (GF256_by_11 (T,T,F,F,T,T,T,T) = (F,T,T,F,T,F,F,F)) /\
  (GF256_by_11 (T,T,F,T,F,F,F,F) = (T,F,T,T,F,F,F,T)) /\
  (GF256_by_11 (T,T,F,T,F,F,F,T) = (T,F,T,T,T,F,T,F)) /\
  (GF256_by_11 (T,T,F,T,F,F,T,F) = (T,F,T,F,F,T,T,T)) /\
  (GF256_by_11 (T,T,F,T,F,F,T,T) = (T,F,T,F,T,T,F,F)) /\
  (GF256_by_11 (T,T,F,T,F,T,F,F) = (T,F,F,T,T,T,F,T)) /\
  (GF256_by_11 (T,T,F,T,F,T,F,T) = (T,F,F,T,F,T,T,F)) /\
  (GF256_by_11 (T,T,F,T,F,T,T,F) = (T,F,F,F,T,F,T,T)) /\
  (GF256_by_11 (T,T,F,T,F,T,T,T) = (T,F,F,F,F,F,F,F)) /\
  (GF256_by_11 (T,T,F,T,T,F,F,F) = (T,T,T,F,T,F,F,T)) /\
  (GF256_by_11 (T,T,F,T,T,F,F,T) = (T,T,T,F,F,F,T,F)) /\
  (GF256_by_11 (T,T,F,T,T,F,T,F) = (T,T,T,T,T,T,T,T)) /\
  (GF256_by_11 (T,T,F,T,T,F,T,T) = (T,T,T,T,F,T,F,F)) /\
  (GF256_by_11 (T,T,F,T,T,T,F,F) = (T,T,F,F,F,T,F,T)) /\
  (GF256_by_11 (T,T,F,T,T,T,F,T) = (T,T,F,F,T,T,T,F)) /\
  (GF256_by_11 (T,T,F,T,T,T,T,F) = (T,T,F,T,F,F,T,T)) /\
  (GF256_by_11 (T,T,F,T,T,T,T,T) = (T,T,F,T,T,F,F,F)) /\
  (GF256_by_11 (T,T,T,F,F,F,F,F) = (F,T,T,T,T,F,T,F)) /\
  (GF256_by_11 (T,T,T,F,F,F,F,T) = (F,T,T,T,F,F,F,T)) /\
  (GF256_by_11 (T,T,T,F,F,F,T,F) = (F,T,T,F,T,T,F,F)) /\
  (GF256_by_11 (T,T,T,F,F,F,T,T) = (F,T,T,F,F,T,T,T)) /\
  (GF256_by_11 (T,T,T,F,F,T,F,F) = (F,T,F,T,F,T,T,F)) /\
  (GF256_by_11 (T,T,T,F,F,T,F,T) = (F,T,F,T,T,T,F,T)) /\
  (GF256_by_11 (T,T,T,F,F,T,T,F) = (F,T,F,F,F,F,F,F)) /\
  (GF256_by_11 (T,T,T,F,F,T,T,T) = (F,T,F,F,T,F,T,T)) /\
  (GF256_by_11 (T,T,T,F,T,F,F,F) = (F,F,T,F,F,F,T,F)) /\
  (GF256_by_11 (T,T,T,F,T,F,F,T) = (F,F,T,F,T,F,F,T)) /\
  (GF256_by_11 (T,T,T,F,T,F,T,F) = (F,F,T,T,F,T,F,F)) /\
  (GF256_by_11 (T,T,T,F,T,F,T,T) = (F,F,T,T,T,T,T,T)) /\
  (GF256_by_11 (T,T,T,F,T,T,F,F) = (F,F,F,F,T,T,T,F)) /\
  (GF256_by_11 (T,T,T,F,T,T,F,T) = (F,F,F,F,F,T,F,T)) /\
  (GF256_by_11 (T,T,T,F,T,T,T,F) = (F,F,F,T,T,F,F,F)) /\
  (GF256_by_11 (T,T,T,F,T,T,T,T) = (F,F,F,T,F,F,T,T)) /\
  (GF256_by_11 (T,T,T,T,F,F,F,F) = (T,T,F,F,T,F,T,F)) /\
  (GF256_by_11 (T,T,T,T,F,F,F,T) = (T,T,F,F,F,F,F,T)) /\
  (GF256_by_11 (T,T,T,T,F,F,T,F) = (T,T,F,T,T,T,F,F)) /\
  (GF256_by_11 (T,T,T,T,F,F,T,T) = (T,T,F,T,F,T,T,T)) /\
  (GF256_by_11 (T,T,T,T,F,T,F,F) = (T,T,T,F,F,T,T,F)) /\
  (GF256_by_11 (T,T,T,T,F,T,F,T) = (T,T,T,F,T,T,F,T)) /\
  (GF256_by_11 (T,T,T,T,F,T,T,F) = (T,T,T,T,F,F,F,F)) /\
  (GF256_by_11 (T,T,T,T,F,T,T,T) = (T,T,T,T,T,F,T,T)) /\
  (GF256_by_11 (T,T,T,T,T,F,F,F) = (T,F,F,T,F,F,T,F)) /\
  (GF256_by_11 (T,T,T,T,T,F,F,T) = (T,F,F,T,T,F,F,T)) /\
  (GF256_by_11 (T,T,T,T,T,F,T,F) = (T,F,F,F,F,T,F,F)) /\
  (GF256_by_11 (T,T,T,T,T,F,T,T) = (T,F,F,F,T,T,T,T)) /\
  (GF256_by_11 (T,T,T,T,T,T,F,F) = (T,F,T,T,T,T,T,F)) /\
  (GF256_by_11 (T,T,T,T,T,T,F,T) = (T,F,T,T,F,T,F,T)) /\
  (GF256_by_11 (T,T,T,T,T,T,T,F) = (T,F,T,F,T,F,F,F)) /\
  (GF256_by_11 (T,T,T,T,T,T,T,T) = (T,F,T,F,F,F,T,T))`;

val GF256_by_13_def = Count.apply Define
 `(GF256_by_13 (F,F,F,F,F,F,F,F) = (F,F,F,F,F,F,F,F)) /\
  (GF256_by_13 (F,F,F,F,F,F,F,T) = (F,F,F,F,T,T,F,T)) /\
  (GF256_by_13 (F,F,F,F,F,F,T,F) = (F,F,F,T,T,F,T,F)) /\
  (GF256_by_13 (F,F,F,F,F,F,T,T) = (F,F,F,T,F,T,T,T)) /\
  (GF256_by_13 (F,F,F,F,F,T,F,F) = (F,F,T,T,F,T,F,F)) /\
  (GF256_by_13 (F,F,F,F,F,T,F,T) = (F,F,T,T,T,F,F,T)) /\
  (GF256_by_13 (F,F,F,F,F,T,T,F) = (F,F,T,F,T,T,T,F)) /\
  (GF256_by_13 (F,F,F,F,F,T,T,T) = (F,F,T,F,F,F,T,T)) /\
  (GF256_by_13 (F,F,F,F,T,F,F,F) = (F,T,T,F,T,F,F,F)) /\
  (GF256_by_13 (F,F,F,F,T,F,F,T) = (F,T,T,F,F,T,F,T)) /\
  (GF256_by_13 (F,F,F,F,T,F,T,F) = (F,T,T,T,F,F,T,F)) /\
  (GF256_by_13 (F,F,F,F,T,F,T,T) = (F,T,T,T,T,T,T,T)) /\
  (GF256_by_13 (F,F,F,F,T,T,F,F) = (F,T,F,T,T,T,F,F)) /\
  (GF256_by_13 (F,F,F,F,T,T,F,T) = (F,T,F,T,F,F,F,T)) /\
  (GF256_by_13 (F,F,F,F,T,T,T,F) = (F,T,F,F,F,T,T,F)) /\
  (GF256_by_13 (F,F,F,F,T,T,T,T) = (F,T,F,F,T,F,T,T)) /\
  (GF256_by_13 (F,F,F,T,F,F,F,F) = (T,T,F,T,F,F,F,F)) /\
  (GF256_by_13 (F,F,F,T,F,F,F,T) = (T,T,F,T,T,T,F,T)) /\
  (GF256_by_13 (F,F,F,T,F,F,T,F) = (T,T,F,F,T,F,T,F)) /\
  (GF256_by_13 (F,F,F,T,F,F,T,T) = (T,T,F,F,F,T,T,T)) /\
  (GF256_by_13 (F,F,F,T,F,T,F,F) = (T,T,T,F,F,T,F,F)) /\
  (GF256_by_13 (F,F,F,T,F,T,F,T) = (T,T,T,F,T,F,F,T)) /\
  (GF256_by_13 (F,F,F,T,F,T,T,F) = (T,T,T,T,T,T,T,F)) /\
  (GF256_by_13 (F,F,F,T,F,T,T,T) = (T,T,T,T,F,F,T,T)) /\
  (GF256_by_13 (F,F,F,T,T,F,F,F) = (T,F,T,T,T,F,F,F)) /\
  (GF256_by_13 (F,F,F,T,T,F,F,T) = (T,F,T,T,F,T,F,T)) /\
  (GF256_by_13 (F,F,F,T,T,F,T,F) = (T,F,T,F,F,F,T,F)) /\
  (GF256_by_13 (F,F,F,T,T,F,T,T) = (T,F,T,F,T,T,T,T)) /\
  (GF256_by_13 (F,F,F,T,T,T,F,F) = (T,F,F,F,T,T,F,F)) /\
  (GF256_by_13 (F,F,F,T,T,T,F,T) = (T,F,F,F,F,F,F,T)) /\
  (GF256_by_13 (F,F,F,T,T,T,T,F) = (T,F,F,T,F,T,T,F)) /\
  (GF256_by_13 (F,F,F,T,T,T,T,T) = (T,F,F,T,T,F,T,T)) /\
  (GF256_by_13 (F,F,T,F,F,F,F,F) = (T,F,T,T,T,F,T,T)) /\
  (GF256_by_13 (F,F,T,F,F,F,F,T) = (T,F,T,T,F,T,T,F)) /\
  (GF256_by_13 (F,F,T,F,F,F,T,F) = (T,F,T,F,F,F,F,T)) /\
  (GF256_by_13 (F,F,T,F,F,F,T,T) = (T,F,T,F,T,T,F,F)) /\
  (GF256_by_13 (F,F,T,F,F,T,F,F) = (T,F,F,F,T,T,T,T)) /\
  (GF256_by_13 (F,F,T,F,F,T,F,T) = (T,F,F,F,F,F,T,F)) /\
  (GF256_by_13 (F,F,T,F,F,T,T,F) = (T,F,F,T,F,T,F,T)) /\
  (GF256_by_13 (F,F,T,F,F,T,T,T) = (T,F,F,T,T,F,F,F)) /\
  (GF256_by_13 (F,F,T,F,T,F,F,F) = (T,T,F,T,F,F,T,T)) /\
  (GF256_by_13 (F,F,T,F,T,F,F,T) = (T,T,F,T,T,T,T,F)) /\
  (GF256_by_13 (F,F,T,F,T,F,T,F) = (T,T,F,F,T,F,F,T)) /\
  (GF256_by_13 (F,F,T,F,T,F,T,T) = (T,T,F,F,F,T,F,F)) /\
  (GF256_by_13 (F,F,T,F,T,T,F,F) = (T,T,T,F,F,T,T,T)) /\
  (GF256_by_13 (F,F,T,F,T,T,F,T) = (T,T,T,F,T,F,T,F)) /\
  (GF256_by_13 (F,F,T,F,T,T,T,F) = (T,T,T,T,T,T,F,T)) /\
  (GF256_by_13 (F,F,T,F,T,T,T,T) = (T,T,T,T,F,F,F,F)) /\
  (GF256_by_13 (F,F,T,T,F,F,F,F) = (F,T,T,F,T,F,T,T)) /\
  (GF256_by_13 (F,F,T,T,F,F,F,T) = (F,T,T,F,F,T,T,F)) /\
  (GF256_by_13 (F,F,T,T,F,F,T,F) = (F,T,T,T,F,F,F,T)) /\
  (GF256_by_13 (F,F,T,T,F,F,T,T) = (F,T,T,T,T,T,F,F)) /\
  (GF256_by_13 (F,F,T,T,F,T,F,F) = (F,T,F,T,T,T,T,T)) /\
  (GF256_by_13 (F,F,T,T,F,T,F,T) = (F,T,F,T,F,F,T,F)) /\
  (GF256_by_13 (F,F,T,T,F,T,T,F) = (F,T,F,F,F,T,F,T)) /\
  (GF256_by_13 (F,F,T,T,F,T,T,T) = (F,T,F,F,T,F,F,F)) /\
  (GF256_by_13 (F,F,T,T,T,F,F,F) = (F,F,F,F,F,F,T,T)) /\
  (GF256_by_13 (F,F,T,T,T,F,F,T) = (F,F,F,F,T,T,T,F)) /\
  (GF256_by_13 (F,F,T,T,T,F,T,F) = (F,F,F,T,T,F,F,T)) /\
  (GF256_by_13 (F,F,T,T,T,F,T,T) = (F,F,F,T,F,T,F,F)) /\
  (GF256_by_13 (F,F,T,T,T,T,F,F) = (F,F,T,T,F,T,T,T)) /\
  (GF256_by_13 (F,F,T,T,T,T,F,T) = (F,F,T,T,T,F,T,F)) /\
  (GF256_by_13 (F,F,T,T,T,T,T,F) = (F,F,T,F,T,T,F,T)) /\
  (GF256_by_13 (F,F,T,T,T,T,T,T) = (F,F,T,F,F,F,F,F)) /\
  (GF256_by_13 (F,T,F,F,F,F,F,F) = (F,T,T,F,T,T,F,T)) /\
  (GF256_by_13 (F,T,F,F,F,F,F,T) = (F,T,T,F,F,F,F,F)) /\
  (GF256_by_13 (F,T,F,F,F,F,T,F) = (F,T,T,T,F,T,T,T)) /\
  (GF256_by_13 (F,T,F,F,F,F,T,T) = (F,T,T,T,T,F,T,F)) /\
  (GF256_by_13 (F,T,F,F,F,T,F,F) = (F,T,F,T,T,F,F,T)) /\
  (GF256_by_13 (F,T,F,F,F,T,F,T) = (F,T,F,T,F,T,F,F)) /\
  (GF256_by_13 (F,T,F,F,F,T,T,F) = (F,T,F,F,F,F,T,T)) /\
  (GF256_by_13 (F,T,F,F,F,T,T,T) = (F,T,F,F,T,T,T,F)) /\
  (GF256_by_13 (F,T,F,F,T,F,F,F) = (F,F,F,F,F,T,F,T)) /\
  (GF256_by_13 (F,T,F,F,T,F,F,T) = (F,F,F,F,T,F,F,F)) /\
  (GF256_by_13 (F,T,F,F,T,F,T,F) = (F,F,F,T,T,T,T,T)) /\
  (GF256_by_13 (F,T,F,F,T,F,T,T) = (F,F,F,T,F,F,T,F)) /\
  (GF256_by_13 (F,T,F,F,T,T,F,F) = (F,F,T,T,F,F,F,T)) /\
  (GF256_by_13 (F,T,F,F,T,T,F,T) = (F,F,T,T,T,T,F,F)) /\
  (GF256_by_13 (F,T,F,F,T,T,T,F) = (F,F,T,F,T,F,T,T)) /\
  (GF256_by_13 (F,T,F,F,T,T,T,T) = (F,F,T,F,F,T,T,F)) /\
  (GF256_by_13 (F,T,F,T,F,F,F,F) = (T,F,T,T,T,T,F,T)) /\
  (GF256_by_13 (F,T,F,T,F,F,F,T) = (T,F,T,T,F,F,F,F)) /\
  (GF256_by_13 (F,T,F,T,F,F,T,F) = (T,F,T,F,F,T,T,T)) /\
  (GF256_by_13 (F,T,F,T,F,F,T,T) = (T,F,T,F,T,F,T,F)) /\
  (GF256_by_13 (F,T,F,T,F,T,F,F) = (T,F,F,F,T,F,F,T)) /\
  (GF256_by_13 (F,T,F,T,F,T,F,T) = (T,F,F,F,F,T,F,F)) /\
  (GF256_by_13 (F,T,F,T,F,T,T,F) = (T,F,F,T,F,F,T,T)) /\
  (GF256_by_13 (F,T,F,T,F,T,T,T) = (T,F,F,T,T,T,T,F)) /\
  (GF256_by_13 (F,T,F,T,T,F,F,F) = (T,T,F,T,F,T,F,T)) /\
  (GF256_by_13 (F,T,F,T,T,F,F,T) = (T,T,F,T,T,F,F,F)) /\
  (GF256_by_13 (F,T,F,T,T,F,T,F) = (T,T,F,F,T,T,T,T)) /\
  (GF256_by_13 (F,T,F,T,T,F,T,T) = (T,T,F,F,F,F,T,F)) /\
  (GF256_by_13 (F,T,F,T,T,T,F,F) = (T,T,T,F,F,F,F,T)) /\
  (GF256_by_13 (F,T,F,T,T,T,F,T) = (T,T,T,F,T,T,F,F)) /\
  (GF256_by_13 (F,T,F,T,T,T,T,F) = (T,T,T,T,T,F,T,T)) /\
  (GF256_by_13 (F,T,F,T,T,T,T,T) = (T,T,T,T,F,T,T,F)) /\
  (GF256_by_13 (F,T,T,F,F,F,F,F) = (T,T,F,T,F,T,T,F)) /\
  (GF256_by_13 (F,T,T,F,F,F,F,T) = (T,T,F,T,T,F,T,T)) /\
  (GF256_by_13 (F,T,T,F,F,F,T,F) = (T,T,F,F,T,T,F,F)) /\
  (GF256_by_13 (F,T,T,F,F,F,T,T) = (T,T,F,F,F,F,F,T)) /\
  (GF256_by_13 (F,T,T,F,F,T,F,F) = (T,T,T,F,F,F,T,F)) /\
  (GF256_by_13 (F,T,T,F,F,T,F,T) = (T,T,T,F,T,T,T,T)) /\
  (GF256_by_13 (F,T,T,F,F,T,T,F) = (T,T,T,T,T,F,F,F)) /\
  (GF256_by_13 (F,T,T,F,F,T,T,T) = (T,T,T,T,F,T,F,T)) /\
  (GF256_by_13 (F,T,T,F,T,F,F,F) = (T,F,T,T,T,T,T,F)) /\
  (GF256_by_13 (F,T,T,F,T,F,F,T) = (T,F,T,T,F,F,T,T)) /\
  (GF256_by_13 (F,T,T,F,T,F,T,F) = (T,F,T,F,F,T,F,F)) /\
  (GF256_by_13 (F,T,T,F,T,F,T,T) = (T,F,T,F,T,F,F,T)) /\
  (GF256_by_13 (F,T,T,F,T,T,F,F) = (T,F,F,F,T,F,T,F)) /\
  (GF256_by_13 (F,T,T,F,T,T,F,T) = (T,F,F,F,F,T,T,T)) /\
  (GF256_by_13 (F,T,T,F,T,T,T,F) = (T,F,F,T,F,F,F,F)) /\
  (GF256_by_13 (F,T,T,F,T,T,T,T) = (T,F,F,T,T,T,F,T)) /\
  (GF256_by_13 (F,T,T,T,F,F,F,F) = (F,F,F,F,F,T,T,F)) /\
  (GF256_by_13 (F,T,T,T,F,F,F,T) = (F,F,F,F,T,F,T,T)) /\
  (GF256_by_13 (F,T,T,T,F,F,T,F) = (F,F,F,T,T,T,F,F)) /\
  (GF256_by_13 (F,T,T,T,F,F,T,T) = (F,F,F,T,F,F,F,T)) /\
  (GF256_by_13 (F,T,T,T,F,T,F,F) = (F,F,T,T,F,F,T,F)) /\
  (GF256_by_13 (F,T,T,T,F,T,F,T) = (F,F,T,T,T,T,T,T)) /\
  (GF256_by_13 (F,T,T,T,F,T,T,F) = (F,F,T,F,T,F,F,F)) /\
  (GF256_by_13 (F,T,T,T,F,T,T,T) = (F,F,T,F,F,T,F,T)) /\
  (GF256_by_13 (F,T,T,T,T,F,F,F) = (F,T,T,F,T,T,T,F)) /\
  (GF256_by_13 (F,T,T,T,T,F,F,T) = (F,T,T,F,F,F,T,T)) /\
  (GF256_by_13 (F,T,T,T,T,F,T,F) = (F,T,T,T,F,T,F,F)) /\
  (GF256_by_13 (F,T,T,T,T,F,T,T) = (F,T,T,T,T,F,F,T)) /\
  (GF256_by_13 (F,T,T,T,T,T,F,F) = (F,T,F,T,T,F,T,F)) /\
  (GF256_by_13 (F,T,T,T,T,T,F,T) = (F,T,F,T,F,T,T,T)) /\
  (GF256_by_13 (F,T,T,T,T,T,T,F) = (F,T,F,F,F,F,F,F)) /\
  (GF256_by_13 (F,T,T,T,T,T,T,T) = (F,T,F,F,T,T,F,T)) /\
  (GF256_by_13 (T,F,F,F,F,F,F,F) = (T,T,F,T,T,F,T,F)) /\
  (GF256_by_13 (T,F,F,F,F,F,F,T) = (T,T,F,T,F,T,T,T)) /\
  (GF256_by_13 (T,F,F,F,F,F,T,F) = (T,T,F,F,F,F,F,F)) /\
  (GF256_by_13 (T,F,F,F,F,F,T,T) = (T,T,F,F,T,T,F,T)) /\
  (GF256_by_13 (T,F,F,F,F,T,F,F) = (T,T,T,F,T,T,T,F)) /\
  (GF256_by_13 (T,F,F,F,F,T,F,T) = (T,T,T,F,F,F,T,T)) /\
  (GF256_by_13 (T,F,F,F,F,T,T,F) = (T,T,T,T,F,T,F,F)) /\
  (GF256_by_13 (T,F,F,F,F,T,T,T) = (T,T,T,T,T,F,F,T)) /\
  (GF256_by_13 (T,F,F,F,T,F,F,F) = (T,F,T,T,F,F,T,F)) /\
  (GF256_by_13 (T,F,F,F,T,F,F,T) = (T,F,T,T,T,T,T,T)) /\
  (GF256_by_13 (T,F,F,F,T,F,T,F) = (T,F,T,F,T,F,F,F)) /\
  (GF256_by_13 (T,F,F,F,T,F,T,T) = (T,F,T,F,F,T,F,T)) /\
  (GF256_by_13 (T,F,F,F,T,T,F,F) = (T,F,F,F,F,T,T,F)) /\
  (GF256_by_13 (T,F,F,F,T,T,F,T) = (T,F,F,F,T,F,T,T)) /\
  (GF256_by_13 (T,F,F,F,T,T,T,F) = (T,F,F,T,T,T,F,F)) /\
  (GF256_by_13 (T,F,F,F,T,T,T,T) = (T,F,F,T,F,F,F,T)) /\
  (GF256_by_13 (T,F,F,T,F,F,F,F) = (F,F,F,F,T,F,T,F)) /\
  (GF256_by_13 (T,F,F,T,F,F,F,T) = (F,F,F,F,F,T,T,T)) /\
  (GF256_by_13 (T,F,F,T,F,F,T,F) = (F,F,F,T,F,F,F,F)) /\
  (GF256_by_13 (T,F,F,T,F,F,T,T) = (F,F,F,T,T,T,F,T)) /\
  (GF256_by_13 (T,F,F,T,F,T,F,F) = (F,F,T,T,T,T,T,F)) /\
  (GF256_by_13 (T,F,F,T,F,T,F,T) = (F,F,T,T,F,F,T,T)) /\
  (GF256_by_13 (T,F,F,T,F,T,T,F) = (F,F,T,F,F,T,F,F)) /\
  (GF256_by_13 (T,F,F,T,F,T,T,T) = (F,F,T,F,T,F,F,T)) /\
  (GF256_by_13 (T,F,F,T,T,F,F,F) = (F,T,T,F,F,F,T,F)) /\
  (GF256_by_13 (T,F,F,T,T,F,F,T) = (F,T,T,F,T,T,T,T)) /\
  (GF256_by_13 (T,F,F,T,T,F,T,F) = (F,T,T,T,T,F,F,F)) /\
  (GF256_by_13 (T,F,F,T,T,F,T,T) = (F,T,T,T,F,T,F,T)) /\
  (GF256_by_13 (T,F,F,T,T,T,F,F) = (F,T,F,T,F,T,T,F)) /\
  (GF256_by_13 (T,F,F,T,T,T,F,T) = (F,T,F,T,T,F,T,T)) /\
  (GF256_by_13 (T,F,F,T,T,T,T,F) = (F,T,F,F,T,T,F,F)) /\
  (GF256_by_13 (T,F,F,T,T,T,T,T) = (F,T,F,F,F,F,F,T)) /\
  (GF256_by_13 (T,F,T,F,F,F,F,F) = (F,T,T,F,F,F,F,T)) /\
  (GF256_by_13 (T,F,T,F,F,F,F,T) = (F,T,T,F,T,T,F,F)) /\
  (GF256_by_13 (T,F,T,F,F,F,T,F) = (F,T,T,T,T,F,T,T)) /\
  (GF256_by_13 (T,F,T,F,F,F,T,T) = (F,T,T,T,F,T,T,F)) /\
  (GF256_by_13 (T,F,T,F,F,T,F,F) = (F,T,F,T,F,T,F,T)) /\
  (GF256_by_13 (T,F,T,F,F,T,F,T) = (F,T,F,T,T,F,F,F)) /\
  (GF256_by_13 (T,F,T,F,F,T,T,F) = (F,T,F,F,T,T,T,T)) /\
  (GF256_by_13 (T,F,T,F,F,T,T,T) = (F,T,F,F,F,F,T,F)) /\
  (GF256_by_13 (T,F,T,F,T,F,F,F) = (F,F,F,F,T,F,F,T)) /\
  (GF256_by_13 (T,F,T,F,T,F,F,T) = (F,F,F,F,F,T,F,F)) /\
  (GF256_by_13 (T,F,T,F,T,F,T,F) = (F,F,F,T,F,F,T,T)) /\
  (GF256_by_13 (T,F,T,F,T,F,T,T) = (F,F,F,T,T,T,T,F)) /\
  (GF256_by_13 (T,F,T,F,T,T,F,F) = (F,F,T,T,T,T,F,T)) /\
  (GF256_by_13 (T,F,T,F,T,T,F,T) = (F,F,T,T,F,F,F,F)) /\
  (GF256_by_13 (T,F,T,F,T,T,T,F) = (F,F,T,F,F,T,T,T)) /\
  (GF256_by_13 (T,F,T,F,T,T,T,T) = (F,F,T,F,T,F,T,F)) /\
  (GF256_by_13 (T,F,T,T,F,F,F,F) = (T,F,T,T,F,F,F,T)) /\
  (GF256_by_13 (T,F,T,T,F,F,F,T) = (T,F,T,T,T,T,F,F)) /\
  (GF256_by_13 (T,F,T,T,F,F,T,F) = (T,F,T,F,T,F,T,T)) /\
  (GF256_by_13 (T,F,T,T,F,F,T,T) = (T,F,T,F,F,T,T,F)) /\
  (GF256_by_13 (T,F,T,T,F,T,F,F) = (T,F,F,F,F,T,F,T)) /\
  (GF256_by_13 (T,F,T,T,F,T,F,T) = (T,F,F,F,T,F,F,F)) /\
  (GF256_by_13 (T,F,T,T,F,T,T,F) = (T,F,F,T,T,T,T,T)) /\
  (GF256_by_13 (T,F,T,T,F,T,T,T) = (T,F,F,T,F,F,T,F)) /\
  (GF256_by_13 (T,F,T,T,T,F,F,F) = (T,T,F,T,T,F,F,T)) /\
  (GF256_by_13 (T,F,T,T,T,F,F,T) = (T,T,F,T,F,T,F,F)) /\
  (GF256_by_13 (T,F,T,T,T,F,T,F) = (T,T,F,F,F,F,T,T)) /\
  (GF256_by_13 (T,F,T,T,T,F,T,T) = (T,T,F,F,T,T,T,F)) /\
  (GF256_by_13 (T,F,T,T,T,T,F,F) = (T,T,T,F,T,T,F,T)) /\
  (GF256_by_13 (T,F,T,T,T,T,F,T) = (T,T,T,F,F,F,F,F)) /\
  (GF256_by_13 (T,F,T,T,T,T,T,F) = (T,T,T,T,F,T,T,T)) /\
  (GF256_by_13 (T,F,T,T,T,T,T,T) = (T,T,T,T,T,F,T,F)) /\
  (GF256_by_13 (T,T,F,F,F,F,F,F) = (T,F,T,T,F,T,T,T)) /\
  (GF256_by_13 (T,T,F,F,F,F,F,T) = (T,F,T,T,T,F,T,F)) /\
  (GF256_by_13 (T,T,F,F,F,F,T,F) = (T,F,T,F,T,T,F,T)) /\
  (GF256_by_13 (T,T,F,F,F,F,T,T) = (T,F,T,F,F,F,F,F)) /\
  (GF256_by_13 (T,T,F,F,F,T,F,F) = (T,F,F,F,F,F,T,T)) /\
  (GF256_by_13 (T,T,F,F,F,T,F,T) = (T,F,F,F,T,T,T,F)) /\
  (GF256_by_13 (T,T,F,F,F,T,T,F) = (T,F,F,T,T,F,F,T)) /\
  (GF256_by_13 (T,T,F,F,F,T,T,T) = (T,F,F,T,F,T,F,F)) /\
  (GF256_by_13 (T,T,F,F,T,F,F,F) = (T,T,F,T,T,T,T,T)) /\
  (GF256_by_13 (T,T,F,F,T,F,F,T) = (T,T,F,T,F,F,T,F)) /\
  (GF256_by_13 (T,T,F,F,T,F,T,F) = (T,T,F,F,F,T,F,T)) /\
  (GF256_by_13 (T,T,F,F,T,F,T,T) = (T,T,F,F,T,F,F,F)) /\
  (GF256_by_13 (T,T,F,F,T,T,F,F) = (T,T,T,F,T,F,T,T)) /\
  (GF256_by_13 (T,T,F,F,T,T,F,T) = (T,T,T,F,F,T,T,F)) /\
  (GF256_by_13 (T,T,F,F,T,T,T,F) = (T,T,T,T,F,F,F,T)) /\
  (GF256_by_13 (T,T,F,F,T,T,T,T) = (T,T,T,T,T,T,F,F)) /\
  (GF256_by_13 (T,T,F,T,F,F,F,F) = (F,T,T,F,F,T,T,T)) /\
  (GF256_by_13 (T,T,F,T,F,F,F,T) = (F,T,T,F,T,F,T,F)) /\
  (GF256_by_13 (T,T,F,T,F,F,T,F) = (F,T,T,T,T,T,F,T)) /\
  (GF256_by_13 (T,T,F,T,F,F,T,T) = (F,T,T,T,F,F,F,F)) /\
  (GF256_by_13 (T,T,F,T,F,T,F,F) = (F,T,F,T,F,F,T,T)) /\
  (GF256_by_13 (T,T,F,T,F,T,F,T) = (F,T,F,T,T,T,T,F)) /\
  (GF256_by_13 (T,T,F,T,F,T,T,F) = (F,T,F,F,T,F,F,T)) /\
  (GF256_by_13 (T,T,F,T,F,T,T,T) = (F,T,F,F,F,T,F,F)) /\
  (GF256_by_13 (T,T,F,T,T,F,F,F) = (F,F,F,F,T,T,T,T)) /\
  (GF256_by_13 (T,T,F,T,T,F,F,T) = (F,F,F,F,F,F,T,F)) /\
  (GF256_by_13 (T,T,F,T,T,F,T,F) = (F,F,F,T,F,T,F,T)) /\
  (GF256_by_13 (T,T,F,T,T,F,T,T) = (F,F,F,T,T,F,F,F)) /\
  (GF256_by_13 (T,T,F,T,T,T,F,F) = (F,F,T,T,T,F,T,T)) /\
  (GF256_by_13 (T,T,F,T,T,T,F,T) = (F,F,T,T,F,T,T,F)) /\
  (GF256_by_13 (T,T,F,T,T,T,T,F) = (F,F,T,F,F,F,F,T)) /\
  (GF256_by_13 (T,T,F,T,T,T,T,T) = (F,F,T,F,T,T,F,F)) /\
  (GF256_by_13 (T,T,T,F,F,F,F,F) = (F,F,F,F,T,T,F,F)) /\
  (GF256_by_13 (T,T,T,F,F,F,F,T) = (F,F,F,F,F,F,F,T)) /\
  (GF256_by_13 (T,T,T,F,F,F,T,F) = (F,F,F,T,F,T,T,F)) /\
  (GF256_by_13 (T,T,T,F,F,F,T,T) = (F,F,F,T,T,F,T,T)) /\
  (GF256_by_13 (T,T,T,F,F,T,F,F) = (F,F,T,T,T,F,F,F)) /\
  (GF256_by_13 (T,T,T,F,F,T,F,T) = (F,F,T,T,F,T,F,T)) /\
  (GF256_by_13 (T,T,T,F,F,T,T,F) = (F,F,T,F,F,F,T,F)) /\
  (GF256_by_13 (T,T,T,F,F,T,T,T) = (F,F,T,F,T,T,T,T)) /\
  (GF256_by_13 (T,T,T,F,T,F,F,F) = (F,T,T,F,F,T,F,F)) /\
  (GF256_by_13 (T,T,T,F,T,F,F,T) = (F,T,T,F,T,F,F,T)) /\
  (GF256_by_13 (T,T,T,F,T,F,T,F) = (F,T,T,T,T,T,T,F)) /\
  (GF256_by_13 (T,T,T,F,T,F,T,T) = (F,T,T,T,F,F,T,T)) /\
  (GF256_by_13 (T,T,T,F,T,T,F,F) = (F,T,F,T,F,F,F,F)) /\
  (GF256_by_13 (T,T,T,F,T,T,F,T) = (F,T,F,T,T,T,F,T)) /\
  (GF256_by_13 (T,T,T,F,T,T,T,F) = (F,T,F,F,T,F,T,F)) /\
  (GF256_by_13 (T,T,T,F,T,T,T,T) = (F,T,F,F,F,T,T,T)) /\
  (GF256_by_13 (T,T,T,T,F,F,F,F) = (T,T,F,T,T,T,F,F)) /\
  (GF256_by_13 (T,T,T,T,F,F,F,T) = (T,T,F,T,F,F,F,T)) /\
  (GF256_by_13 (T,T,T,T,F,F,T,F) = (T,T,F,F,F,T,T,F)) /\
  (GF256_by_13 (T,T,T,T,F,F,T,T) = (T,T,F,F,T,F,T,T)) /\
  (GF256_by_13 (T,T,T,T,F,T,F,F) = (T,T,T,F,T,F,F,F)) /\
  (GF256_by_13 (T,T,T,T,F,T,F,T) = (T,T,T,F,F,T,F,T)) /\
  (GF256_by_13 (T,T,T,T,F,T,T,F) = (T,T,T,T,F,F,T,F)) /\
  (GF256_by_13 (T,T,T,T,F,T,T,T) = (T,T,T,T,T,T,T,T)) /\
  (GF256_by_13 (T,T,T,T,T,F,F,F) = (T,F,T,T,F,T,F,F)) /\
  (GF256_by_13 (T,T,T,T,T,F,F,T) = (T,F,T,T,T,F,F,T)) /\
  (GF256_by_13 (T,T,T,T,T,F,T,F) = (T,F,T,F,T,T,T,F)) /\
  (GF256_by_13 (T,T,T,T,T,F,T,T) = (T,F,T,F,F,F,T,T)) /\
  (GF256_by_13 (T,T,T,T,T,T,F,F) = (T,F,F,F,F,F,F,F)) /\
  (GF256_by_13 (T,T,T,T,T,T,F,T) = (T,F,F,F,T,T,F,T)) /\
  (GF256_by_13 (T,T,T,T,T,T,T,F) = (T,F,F,T,T,F,T,F)) /\
  (GF256_by_13 (T,T,T,T,T,T,T,T) = (T,F,F,T,F,T,T,T))`;

val GF256_by_14_def = Count.apply Define
 `(GF256_by_14 (F,F,F,F,F,F,F,F) = (F,F,F,F,F,F,F,F)) /\
  (GF256_by_14 (F,F,F,F,F,F,F,T) = (F,F,F,F,T,T,T,F)) /\
  (GF256_by_14 (F,F,F,F,F,F,T,F) = (F,F,F,T,T,T,F,F)) /\
  (GF256_by_14 (F,F,F,F,F,F,T,T) = (F,F,F,T,F,F,T,F)) /\
  (GF256_by_14 (F,F,F,F,F,T,F,F) = (F,F,T,T,T,F,F,F)) /\
  (GF256_by_14 (F,F,F,F,F,T,F,T) = (F,F,T,T,F,T,T,F)) /\
  (GF256_by_14 (F,F,F,F,F,T,T,F) = (F,F,T,F,F,T,F,F)) /\
  (GF256_by_14 (F,F,F,F,F,T,T,T) = (F,F,T,F,T,F,T,F)) /\
  (GF256_by_14 (F,F,F,F,T,F,F,F) = (F,T,T,T,F,F,F,F)) /\
  (GF256_by_14 (F,F,F,F,T,F,F,T) = (F,T,T,T,T,T,T,F)) /\
  (GF256_by_14 (F,F,F,F,T,F,T,F) = (F,T,T,F,T,T,F,F)) /\
  (GF256_by_14 (F,F,F,F,T,F,T,T) = (F,T,T,F,F,F,T,F)) /\
  (GF256_by_14 (F,F,F,F,T,T,F,F) = (F,T,F,F,T,F,F,F)) /\
  (GF256_by_14 (F,F,F,F,T,T,F,T) = (F,T,F,F,F,T,T,F)) /\
  (GF256_by_14 (F,F,F,F,T,T,T,F) = (F,T,F,T,F,T,F,F)) /\
  (GF256_by_14 (F,F,F,F,T,T,T,T) = (F,T,F,T,T,F,T,F)) /\
  (GF256_by_14 (F,F,F,T,F,F,F,F) = (T,T,T,F,F,F,F,F)) /\
  (GF256_by_14 (F,F,F,T,F,F,F,T) = (T,T,T,F,T,T,T,F)) /\
  (GF256_by_14 (F,F,F,T,F,F,T,F) = (T,T,T,T,T,T,F,F)) /\
  (GF256_by_14 (F,F,F,T,F,F,T,T) = (T,T,T,T,F,F,T,F)) /\
  (GF256_by_14 (F,F,F,T,F,T,F,F) = (T,T,F,T,T,F,F,F)) /\
  (GF256_by_14 (F,F,F,T,F,T,F,T) = (T,T,F,T,F,T,T,F)) /\
  (GF256_by_14 (F,F,F,T,F,T,T,F) = (T,T,F,F,F,T,F,F)) /\
  (GF256_by_14 (F,F,F,T,F,T,T,T) = (T,T,F,F,T,F,T,F)) /\
  (GF256_by_14 (F,F,F,T,T,F,F,F) = (T,F,F,T,F,F,F,F)) /\
  (GF256_by_14 (F,F,F,T,T,F,F,T) = (T,F,F,T,T,T,T,F)) /\
  (GF256_by_14 (F,F,F,T,T,F,T,F) = (T,F,F,F,T,T,F,F)) /\
  (GF256_by_14 (F,F,F,T,T,F,T,T) = (T,F,F,F,F,F,T,F)) /\
  (GF256_by_14 (F,F,F,T,T,T,F,F) = (T,F,T,F,T,F,F,F)) /\
  (GF256_by_14 (F,F,F,T,T,T,F,T) = (T,F,T,F,F,T,T,F)) /\
  (GF256_by_14 (F,F,F,T,T,T,T,F) = (T,F,T,T,F,T,F,F)) /\
  (GF256_by_14 (F,F,F,T,T,T,T,T) = (T,F,T,T,T,F,T,F)) /\
  (GF256_by_14 (F,F,T,F,F,F,F,F) = (T,T,F,T,T,F,T,T)) /\
  (GF256_by_14 (F,F,T,F,F,F,F,T) = (T,T,F,T,F,T,F,T)) /\
  (GF256_by_14 (F,F,T,F,F,F,T,F) = (T,T,F,F,F,T,T,T)) /\
  (GF256_by_14 (F,F,T,F,F,F,T,T) = (T,T,F,F,T,F,F,T)) /\
  (GF256_by_14 (F,F,T,F,F,T,F,F) = (T,T,T,F,F,F,T,T)) /\
  (GF256_by_14 (F,F,T,F,F,T,F,T) = (T,T,T,F,T,T,F,T)) /\
  (GF256_by_14 (F,F,T,F,F,T,T,F) = (T,T,T,T,T,T,T,T)) /\
  (GF256_by_14 (F,F,T,F,F,T,T,T) = (T,T,T,T,F,F,F,T)) /\
  (GF256_by_14 (F,F,T,F,T,F,F,F) = (T,F,T,F,T,F,T,T)) /\
  (GF256_by_14 (F,F,T,F,T,F,F,T) = (T,F,T,F,F,T,F,T)) /\
  (GF256_by_14 (F,F,T,F,T,F,T,F) = (T,F,T,T,F,T,T,T)) /\
  (GF256_by_14 (F,F,T,F,T,F,T,T) = (T,F,T,T,T,F,F,T)) /\
  (GF256_by_14 (F,F,T,F,T,T,F,F) = (T,F,F,T,F,F,T,T)) /\
  (GF256_by_14 (F,F,T,F,T,T,F,T) = (T,F,F,T,T,T,F,T)) /\
  (GF256_by_14 (F,F,T,F,T,T,T,F) = (T,F,F,F,T,T,T,T)) /\
  (GF256_by_14 (F,F,T,F,T,T,T,T) = (T,F,F,F,F,F,F,T)) /\
  (GF256_by_14 (F,F,T,T,F,F,F,F) = (F,F,T,T,T,F,T,T)) /\
  (GF256_by_14 (F,F,T,T,F,F,F,T) = (F,F,T,T,F,T,F,T)) /\
  (GF256_by_14 (F,F,T,T,F,F,T,F) = (F,F,T,F,F,T,T,T)) /\
  (GF256_by_14 (F,F,T,T,F,F,T,T) = (F,F,T,F,T,F,F,T)) /\
  (GF256_by_14 (F,F,T,T,F,T,F,F) = (F,F,F,F,F,F,T,T)) /\
  (GF256_by_14 (F,F,T,T,F,T,F,T) = (F,F,F,F,T,T,F,T)) /\
  (GF256_by_14 (F,F,T,T,F,T,T,F) = (F,F,F,T,T,T,T,T)) /\
  (GF256_by_14 (F,F,T,T,F,T,T,T) = (F,F,F,T,F,F,F,T)) /\
  (GF256_by_14 (F,F,T,T,T,F,F,F) = (F,T,F,F,T,F,T,T)) /\
  (GF256_by_14 (F,F,T,T,T,F,F,T) = (F,T,F,F,F,T,F,T)) /\
  (GF256_by_14 (F,F,T,T,T,F,T,F) = (F,T,F,T,F,T,T,T)) /\
  (GF256_by_14 (F,F,T,T,T,F,T,T) = (F,T,F,T,T,F,F,T)) /\
  (GF256_by_14 (F,F,T,T,T,T,F,F) = (F,T,T,T,F,F,T,T)) /\
  (GF256_by_14 (F,F,T,T,T,T,F,T) = (F,T,T,T,T,T,F,T)) /\
  (GF256_by_14 (F,F,T,T,T,T,T,F) = (F,T,T,F,T,T,T,T)) /\
  (GF256_by_14 (F,F,T,T,T,T,T,T) = (F,T,T,F,F,F,F,T)) /\
  (GF256_by_14 (F,T,F,F,F,F,F,F) = (T,F,T,F,T,T,F,T)) /\
  (GF256_by_14 (F,T,F,F,F,F,F,T) = (T,F,T,F,F,F,T,T)) /\
  (GF256_by_14 (F,T,F,F,F,F,T,F) = (T,F,T,T,F,F,F,T)) /\
  (GF256_by_14 (F,T,F,F,F,F,T,T) = (T,F,T,T,T,T,T,T)) /\
  (GF256_by_14 (F,T,F,F,F,T,F,F) = (T,F,F,T,F,T,F,T)) /\
  (GF256_by_14 (F,T,F,F,F,T,F,T) = (T,F,F,T,T,F,T,T)) /\
  (GF256_by_14 (F,T,F,F,F,T,T,F) = (T,F,F,F,T,F,F,T)) /\
  (GF256_by_14 (F,T,F,F,F,T,T,T) = (T,F,F,F,F,T,T,T)) /\
  (GF256_by_14 (F,T,F,F,T,F,F,F) = (T,T,F,T,T,T,F,T)) /\
  (GF256_by_14 (F,T,F,F,T,F,F,T) = (T,T,F,T,F,F,T,T)) /\
  (GF256_by_14 (F,T,F,F,T,F,T,F) = (T,T,F,F,F,F,F,T)) /\
  (GF256_by_14 (F,T,F,F,T,F,T,T) = (T,T,F,F,T,T,T,T)) /\
  (GF256_by_14 (F,T,F,F,T,T,F,F) = (T,T,T,F,F,T,F,T)) /\
  (GF256_by_14 (F,T,F,F,T,T,F,T) = (T,T,T,F,T,F,T,T)) /\
  (GF256_by_14 (F,T,F,F,T,T,T,F) = (T,T,T,T,T,F,F,T)) /\
  (GF256_by_14 (F,T,F,F,T,T,T,T) = (T,T,T,T,F,T,T,T)) /\
  (GF256_by_14 (F,T,F,T,F,F,F,F) = (F,T,F,F,T,T,F,T)) /\
  (GF256_by_14 (F,T,F,T,F,F,F,T) = (F,T,F,F,F,F,T,T)) /\
  (GF256_by_14 (F,T,F,T,F,F,T,F) = (F,T,F,T,F,F,F,T)) /\
  (GF256_by_14 (F,T,F,T,F,F,T,T) = (F,T,F,T,T,T,T,T)) /\
  (GF256_by_14 (F,T,F,T,F,T,F,F) = (F,T,T,T,F,T,F,T)) /\
  (GF256_by_14 (F,T,F,T,F,T,F,T) = (F,T,T,T,T,F,T,T)) /\
  (GF256_by_14 (F,T,F,T,F,T,T,F) = (F,T,T,F,T,F,F,T)) /\
  (GF256_by_14 (F,T,F,T,F,T,T,T) = (F,T,T,F,F,T,T,T)) /\
  (GF256_by_14 (F,T,F,T,T,F,F,F) = (F,F,T,T,T,T,F,T)) /\
  (GF256_by_14 (F,T,F,T,T,F,F,T) = (F,F,T,T,F,F,T,T)) /\
  (GF256_by_14 (F,T,F,T,T,F,T,F) = (F,F,T,F,F,F,F,T)) /\
  (GF256_by_14 (F,T,F,T,T,F,T,T) = (F,F,T,F,T,T,T,T)) /\
  (GF256_by_14 (F,T,F,T,T,T,F,F) = (F,F,F,F,F,T,F,T)) /\
  (GF256_by_14 (F,T,F,T,T,T,F,T) = (F,F,F,F,T,F,T,T)) /\
  (GF256_by_14 (F,T,F,T,T,T,T,F) = (F,F,F,T,T,F,F,T)) /\
  (GF256_by_14 (F,T,F,T,T,T,T,T) = (F,F,F,T,F,T,T,T)) /\
  (GF256_by_14 (F,T,T,F,F,F,F,F) = (F,T,T,T,F,T,T,F)) /\
  (GF256_by_14 (F,T,T,F,F,F,F,T) = (F,T,T,T,T,F,F,F)) /\
  (GF256_by_14 (F,T,T,F,F,F,T,F) = (F,T,T,F,T,F,T,F)) /\
  (GF256_by_14 (F,T,T,F,F,F,T,T) = (F,T,T,F,F,T,F,F)) /\
  (GF256_by_14 (F,T,T,F,F,T,F,F) = (F,T,F,F,T,T,T,F)) /\
  (GF256_by_14 (F,T,T,F,F,T,F,T) = (F,T,F,F,F,F,F,F)) /\
  (GF256_by_14 (F,T,T,F,F,T,T,F) = (F,T,F,T,F,F,T,F)) /\
  (GF256_by_14 (F,T,T,F,F,T,T,T) = (F,T,F,T,T,T,F,F)) /\
  (GF256_by_14 (F,T,T,F,T,F,F,F) = (F,F,F,F,F,T,T,F)) /\
  (GF256_by_14 (F,T,T,F,T,F,F,T) = (F,F,F,F,T,F,F,F)) /\
  (GF256_by_14 (F,T,T,F,T,F,T,F) = (F,F,F,T,T,F,T,F)) /\
  (GF256_by_14 (F,T,T,F,T,F,T,T) = (F,F,F,T,F,T,F,F)) /\
  (GF256_by_14 (F,T,T,F,T,T,F,F) = (F,F,T,T,T,T,T,F)) /\
  (GF256_by_14 (F,T,T,F,T,T,F,T) = (F,F,T,T,F,F,F,F)) /\
  (GF256_by_14 (F,T,T,F,T,T,T,F) = (F,F,T,F,F,F,T,F)) /\
  (GF256_by_14 (F,T,T,F,T,T,T,T) = (F,F,T,F,T,T,F,F)) /\
  (GF256_by_14 (F,T,T,T,F,F,F,F) = (T,F,F,T,F,T,T,F)) /\
  (GF256_by_14 (F,T,T,T,F,F,F,T) = (T,F,F,T,T,F,F,F)) /\
  (GF256_by_14 (F,T,T,T,F,F,T,F) = (T,F,F,F,T,F,T,F)) /\
  (GF256_by_14 (F,T,T,T,F,F,T,T) = (T,F,F,F,F,T,F,F)) /\
  (GF256_by_14 (F,T,T,T,F,T,F,F) = (T,F,T,F,T,T,T,F)) /\
  (GF256_by_14 (F,T,T,T,F,T,F,T) = (T,F,T,F,F,F,F,F)) /\
  (GF256_by_14 (F,T,T,T,F,T,T,F) = (T,F,T,T,F,F,T,F)) /\
  (GF256_by_14 (F,T,T,T,F,T,T,T) = (T,F,T,T,T,T,F,F)) /\
  (GF256_by_14 (F,T,T,T,T,F,F,F) = (T,T,T,F,F,T,T,F)) /\
  (GF256_by_14 (F,T,T,T,T,F,F,T) = (T,T,T,F,T,F,F,F)) /\
  (GF256_by_14 (F,T,T,T,T,F,T,F) = (T,T,T,T,T,F,T,F)) /\
  (GF256_by_14 (F,T,T,T,T,F,T,T) = (T,T,T,T,F,T,F,F)) /\
  (GF256_by_14 (F,T,T,T,T,T,F,F) = (T,T,F,T,T,T,T,F)) /\
  (GF256_by_14 (F,T,T,T,T,T,F,T) = (T,T,F,T,F,F,F,F)) /\
  (GF256_by_14 (F,T,T,T,T,T,T,F) = (T,T,F,F,F,F,T,F)) /\
  (GF256_by_14 (F,T,T,T,T,T,T,T) = (T,T,F,F,T,T,F,F)) /\
  (GF256_by_14 (T,F,F,F,F,F,F,F) = (F,T,F,F,F,F,F,T)) /\
  (GF256_by_14 (T,F,F,F,F,F,F,T) = (F,T,F,F,T,T,T,T)) /\
  (GF256_by_14 (T,F,F,F,F,F,T,F) = (F,T,F,T,T,T,F,T)) /\
  (GF256_by_14 (T,F,F,F,F,F,T,T) = (F,T,F,T,F,F,T,T)) /\
  (GF256_by_14 (T,F,F,F,F,T,F,F) = (F,T,T,T,T,F,F,T)) /\
  (GF256_by_14 (T,F,F,F,F,T,F,T) = (F,T,T,T,F,T,T,T)) /\
  (GF256_by_14 (T,F,F,F,F,T,T,F) = (F,T,T,F,F,T,F,T)) /\
  (GF256_by_14 (T,F,F,F,F,T,T,T) = (F,T,T,F,T,F,T,T)) /\
  (GF256_by_14 (T,F,F,F,T,F,F,F) = (F,F,T,T,F,F,F,T)) /\
  (GF256_by_14 (T,F,F,F,T,F,F,T) = (F,F,T,T,T,T,T,T)) /\
  (GF256_by_14 (T,F,F,F,T,F,T,F) = (F,F,T,F,T,T,F,T)) /\
  (GF256_by_14 (T,F,F,F,T,F,T,T) = (F,F,T,F,F,F,T,T)) /\
  (GF256_by_14 (T,F,F,F,T,T,F,F) = (F,F,F,F,T,F,F,T)) /\
  (GF256_by_14 (T,F,F,F,T,T,F,T) = (F,F,F,F,F,T,T,T)) /\
  (GF256_by_14 (T,F,F,F,T,T,T,F) = (F,F,F,T,F,T,F,T)) /\
  (GF256_by_14 (T,F,F,F,T,T,T,T) = (F,F,F,T,T,F,T,T)) /\
  (GF256_by_14 (T,F,F,T,F,F,F,F) = (T,F,T,F,F,F,F,T)) /\
  (GF256_by_14 (T,F,F,T,F,F,F,T) = (T,F,T,F,T,T,T,T)) /\
  (GF256_by_14 (T,F,F,T,F,F,T,F) = (T,F,T,T,T,T,F,T)) /\
  (GF256_by_14 (T,F,F,T,F,F,T,T) = (T,F,T,T,F,F,T,T)) /\
  (GF256_by_14 (T,F,F,T,F,T,F,F) = (T,F,F,T,T,F,F,T)) /\
  (GF256_by_14 (T,F,F,T,F,T,F,T) = (T,F,F,T,F,T,T,T)) /\
  (GF256_by_14 (T,F,F,T,F,T,T,F) = (T,F,F,F,F,T,F,T)) /\
  (GF256_by_14 (T,F,F,T,F,T,T,T) = (T,F,F,F,T,F,T,T)) /\
  (GF256_by_14 (T,F,F,T,T,F,F,F) = (T,T,F,T,F,F,F,T)) /\
  (GF256_by_14 (T,F,F,T,T,F,F,T) = (T,T,F,T,T,T,T,T)) /\
  (GF256_by_14 (T,F,F,T,T,F,T,F) = (T,T,F,F,T,T,F,T)) /\
  (GF256_by_14 (T,F,F,T,T,F,T,T) = (T,T,F,F,F,F,T,T)) /\
  (GF256_by_14 (T,F,F,T,T,T,F,F) = (T,T,T,F,T,F,F,T)) /\
  (GF256_by_14 (T,F,F,T,T,T,F,T) = (T,T,T,F,F,T,T,T)) /\
  (GF256_by_14 (T,F,F,T,T,T,T,F) = (T,T,T,T,F,T,F,T)) /\
  (GF256_by_14 (T,F,F,T,T,T,T,T) = (T,T,T,T,T,F,T,T)) /\
  (GF256_by_14 (T,F,T,F,F,F,F,F) = (T,F,F,T,T,F,T,F)) /\
  (GF256_by_14 (T,F,T,F,F,F,F,T) = (T,F,F,T,F,T,F,F)) /\
  (GF256_by_14 (T,F,T,F,F,F,T,F) = (T,F,F,F,F,T,T,F)) /\
  (GF256_by_14 (T,F,T,F,F,F,T,T) = (T,F,F,F,T,F,F,F)) /\
  (GF256_by_14 (T,F,T,F,F,T,F,F) = (T,F,T,F,F,F,T,F)) /\
  (GF256_by_14 (T,F,T,F,F,T,F,T) = (T,F,T,F,T,T,F,F)) /\
  (GF256_by_14 (T,F,T,F,F,T,T,F) = (T,F,T,T,T,T,T,F)) /\
  (GF256_by_14 (T,F,T,F,F,T,T,T) = (T,F,T,T,F,F,F,F)) /\
  (GF256_by_14 (T,F,T,F,T,F,F,F) = (T,T,T,F,T,F,T,F)) /\
  (GF256_by_14 (T,F,T,F,T,F,F,T) = (T,T,T,F,F,T,F,F)) /\
  (GF256_by_14 (T,F,T,F,T,F,T,F) = (T,T,T,T,F,T,T,F)) /\
  (GF256_by_14 (T,F,T,F,T,F,T,T) = (T,T,T,T,T,F,F,F)) /\
  (GF256_by_14 (T,F,T,F,T,T,F,F) = (T,T,F,T,F,F,T,F)) /\
  (GF256_by_14 (T,F,T,F,T,T,F,T) = (T,T,F,T,T,T,F,F)) /\
  (GF256_by_14 (T,F,T,F,T,T,T,F) = (T,T,F,F,T,T,T,F)) /\
  (GF256_by_14 (T,F,T,F,T,T,T,T) = (T,T,F,F,F,F,F,F)) /\
  (GF256_by_14 (T,F,T,T,F,F,F,F) = (F,T,T,T,T,F,T,F)) /\
  (GF256_by_14 (T,F,T,T,F,F,F,T) = (F,T,T,T,F,T,F,F)) /\
  (GF256_by_14 (T,F,T,T,F,F,T,F) = (F,T,T,F,F,T,T,F)) /\
  (GF256_by_14 (T,F,T,T,F,F,T,T) = (F,T,T,F,T,F,F,F)) /\
  (GF256_by_14 (T,F,T,T,F,T,F,F) = (F,T,F,F,F,F,T,F)) /\
  (GF256_by_14 (T,F,T,T,F,T,F,T) = (F,T,F,F,T,T,F,F)) /\
  (GF256_by_14 (T,F,T,T,F,T,T,F) = (F,T,F,T,T,T,T,F)) /\
  (GF256_by_14 (T,F,T,T,F,T,T,T) = (F,T,F,T,F,F,F,F)) /\
  (GF256_by_14 (T,F,T,T,T,F,F,F) = (F,F,F,F,T,F,T,F)) /\
  (GF256_by_14 (T,F,T,T,T,F,F,T) = (F,F,F,F,F,T,F,F)) /\
  (GF256_by_14 (T,F,T,T,T,F,T,F) = (F,F,F,T,F,T,T,F)) /\
  (GF256_by_14 (T,F,T,T,T,F,T,T) = (F,F,F,T,T,F,F,F)) /\
  (GF256_by_14 (T,F,T,T,T,T,F,F) = (F,F,T,T,F,F,T,F)) /\
  (GF256_by_14 (T,F,T,T,T,T,F,T) = (F,F,T,T,T,T,F,F)) /\
  (GF256_by_14 (T,F,T,T,T,T,T,F) = (F,F,T,F,T,T,T,F)) /\
  (GF256_by_14 (T,F,T,T,T,T,T,T) = (F,F,T,F,F,F,F,F)) /\
  (GF256_by_14 (T,T,F,F,F,F,F,F) = (T,T,T,F,T,T,F,F)) /\
  (GF256_by_14 (T,T,F,F,F,F,F,T) = (T,T,T,F,F,F,T,F)) /\
  (GF256_by_14 (T,T,F,F,F,F,T,F) = (T,T,T,T,F,F,F,F)) /\
  (GF256_by_14 (T,T,F,F,F,F,T,T) = (T,T,T,T,T,T,T,F)) /\
  (GF256_by_14 (T,T,F,F,F,T,F,F) = (T,T,F,T,F,T,F,F)) /\
  (GF256_by_14 (T,T,F,F,F,T,F,T) = (T,T,F,T,T,F,T,F)) /\
  (GF256_by_14 (T,T,F,F,F,T,T,F) = (T,T,F,F,T,F,F,F)) /\
  (GF256_by_14 (T,T,F,F,F,T,T,T) = (T,T,F,F,F,T,T,F)) /\
  (GF256_by_14 (T,T,F,F,T,F,F,F) = (T,F,F,T,T,T,F,F)) /\
  (GF256_by_14 (T,T,F,F,T,F,F,T) = (T,F,F,T,F,F,T,F)) /\
  (GF256_by_14 (T,T,F,F,T,F,T,F) = (T,F,F,F,F,F,F,F)) /\
  (GF256_by_14 (T,T,F,F,T,F,T,T) = (T,F,F,F,T,T,T,F)) /\
  (GF256_by_14 (T,T,F,F,T,T,F,F) = (T,F,T,F,F,T,F,F)) /\
  (GF256_by_14 (T,T,F,F,T,T,F,T) = (T,F,T,F,T,F,T,F)) /\
  (GF256_by_14 (T,T,F,F,T,T,T,F) = (T,F,T,T,T,F,F,F)) /\
  (GF256_by_14 (T,T,F,F,T,T,T,T) = (T,F,T,T,F,T,T,F)) /\
  (GF256_by_14 (T,T,F,T,F,F,F,F) = (F,F,F,F,T,T,F,F)) /\
  (GF256_by_14 (T,T,F,T,F,F,F,T) = (F,F,F,F,F,F,T,F)) /\
  (GF256_by_14 (T,T,F,T,F,F,T,F) = (F,F,F,T,F,F,F,F)) /\
  (GF256_by_14 (T,T,F,T,F,F,T,T) = (F,F,F,T,T,T,T,F)) /\
  (GF256_by_14 (T,T,F,T,F,T,F,F) = (F,F,T,T,F,T,F,F)) /\
  (GF256_by_14 (T,T,F,T,F,T,F,T) = (F,F,T,T,T,F,T,F)) /\
  (GF256_by_14 (T,T,F,T,F,T,T,F) = (F,F,T,F,T,F,F,F)) /\
  (GF256_by_14 (T,T,F,T,F,T,T,T) = (F,F,T,F,F,T,T,F)) /\
  (GF256_by_14 (T,T,F,T,T,F,F,F) = (F,T,T,T,T,T,F,F)) /\
  (GF256_by_14 (T,T,F,T,T,F,F,T) = (F,T,T,T,F,F,T,F)) /\
  (GF256_by_14 (T,T,F,T,T,F,T,F) = (F,T,T,F,F,F,F,F)) /\
  (GF256_by_14 (T,T,F,T,T,F,T,T) = (F,T,T,F,T,T,T,F)) /\
  (GF256_by_14 (T,T,F,T,T,T,F,F) = (F,T,F,F,F,T,F,F)) /\
  (GF256_by_14 (T,T,F,T,T,T,F,T) = (F,T,F,F,T,F,T,F)) /\
  (GF256_by_14 (T,T,F,T,T,T,T,F) = (F,T,F,T,T,F,F,F)) /\
  (GF256_by_14 (T,T,F,T,T,T,T,T) = (F,T,F,T,F,T,T,F)) /\
  (GF256_by_14 (T,T,T,F,F,F,F,F) = (F,F,T,T,F,T,T,T)) /\
  (GF256_by_14 (T,T,T,F,F,F,F,T) = (F,F,T,T,T,F,F,T)) /\
  (GF256_by_14 (T,T,T,F,F,F,T,F) = (F,F,T,F,T,F,T,T)) /\
  (GF256_by_14 (T,T,T,F,F,F,T,T) = (F,F,T,F,F,T,F,T)) /\
  (GF256_by_14 (T,T,T,F,F,T,F,F) = (F,F,F,F,T,T,T,T)) /\
  (GF256_by_14 (T,T,T,F,F,T,F,T) = (F,F,F,F,F,F,F,T)) /\
  (GF256_by_14 (T,T,T,F,F,T,T,F) = (F,F,F,T,F,F,T,T)) /\
  (GF256_by_14 (T,T,T,F,F,T,T,T) = (F,F,F,T,T,T,F,T)) /\
  (GF256_by_14 (T,T,T,F,T,F,F,F) = (F,T,F,F,F,T,T,T)) /\
  (GF256_by_14 (T,T,T,F,T,F,F,T) = (F,T,F,F,T,F,F,T)) /\
  (GF256_by_14 (T,T,T,F,T,F,T,F) = (F,T,F,T,T,F,T,T)) /\
  (GF256_by_14 (T,T,T,F,T,F,T,T) = (F,T,F,T,F,T,F,T)) /\
  (GF256_by_14 (T,T,T,F,T,T,F,F) = (F,T,T,T,T,T,T,T)) /\
  (GF256_by_14 (T,T,T,F,T,T,F,T) = (F,T,T,T,F,F,F,T)) /\
  (GF256_by_14 (T,T,T,F,T,T,T,F) = (F,T,T,F,F,F,T,T)) /\
  (GF256_by_14 (T,T,T,F,T,T,T,T) = (F,T,T,F,T,T,F,T)) /\
  (GF256_by_14 (T,T,T,T,F,F,F,F) = (T,T,F,T,F,T,T,T)) /\
  (GF256_by_14 (T,T,T,T,F,F,F,T) = (T,T,F,T,T,F,F,T)) /\
  (GF256_by_14 (T,T,T,T,F,F,T,F) = (T,T,F,F,T,F,T,T)) /\
  (GF256_by_14 (T,T,T,T,F,F,T,T) = (T,T,F,F,F,T,F,T)) /\
  (GF256_by_14 (T,T,T,T,F,T,F,F) = (T,T,T,F,T,T,T,T)) /\
  (GF256_by_14 (T,T,T,T,F,T,F,T) = (T,T,T,F,F,F,F,T)) /\
  (GF256_by_14 (T,T,T,T,F,T,T,F) = (T,T,T,T,F,F,T,T)) /\
  (GF256_by_14 (T,T,T,T,F,T,T,T) = (T,T,T,T,T,T,F,T)) /\
  (GF256_by_14 (T,T,T,T,T,F,F,F) = (T,F,T,F,F,T,T,T)) /\
  (GF256_by_14 (T,T,T,T,T,F,F,T) = (T,F,T,F,T,F,F,T)) /\
  (GF256_by_14 (T,T,T,T,T,F,T,F) = (T,F,T,T,T,F,T,T)) /\
  (GF256_by_14 (T,T,T,T,T,F,T,T) = (T,F,T,T,F,T,F,T)) /\
  (GF256_by_14 (T,T,T,T,T,T,F,F) = (T,F,F,T,T,T,T,T)) /\
  (GF256_by_14 (T,T,T,T,T,T,F,T) = (T,F,F,T,F,F,F,T)) /\
  (GF256_by_14 (T,T,T,T,T,T,T,F) = (T,F,F,F,F,F,T,T)) /\
  (GF256_by_14 (T,T,T,T,T,T,T,T) = (T,F,F,F,T,T,F,T))`;

val Sbox_Inversion = Q.store_thm
("Sbox_Inversion",
 `!w:word8. InvSbox (Sbox w) = w`,
 SIMP_TAC std_ss [FORALL_BYTE_BITS, Sbox_def, InvSbox_def]);

val _ = export_theory();
